chore: small golfs, mostly using gcongr

Author: grunweg

SphereEversion/InductiveConstructions.lean

@@ -382,7 +382,7 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ
           rw [mem_Ici]
           congr
           rw [← mul_T_succ_sub i.toNat]
-        exact mul_le_mul_of_nonneg_left (sub_le_sub_right ht _) (pow_nonneg zero_le_two _)
+        gcongr
       · push_neg
         apply T_lt_succ
     · rintro j hj ⟨t, x⟩ (rfl : t = 1)
@@ -397,7 +397,8 @@ theorem inductive_htpy_construction' {X Y : Type*} [TopologicalSpace X] {N : ℕ
       apply congr_fun (hfutur_F'.self_of_nhdsSet ..)
       rw [mem_Ici]
       conv => congr; skip; rw [← mul_T_succ_sub i.toNat]
-      exact mul_le_mul_of_nonneg_left (sub_le_sub_right (T_lt _).le _) (pow_nonneg zero_le_two _)
+      gcongr
+      exact (T_lt _).le
     · rintro ⟨t, x⟩ htx
       simp only [prodMk_mem_set_prod_eq, mem_Ici, not_and_or, not_le] at htx
       obtain (ht | hx) := htx

SphereEversion/ToMathlib/Equivariant.lean

@@ -58,13 +58,13 @@ protected theorem monotone (h : MonotoneOn φ I) : Monotone φ := fun x y hxy 
   · rw [h2]
     refine add_le_add_right (h (unitInterval.fract_mem _) (unitInterval.fract_mem _) ?_) _
     simp_rw [fract, h2]
-    exact sub_le_sub_right hxy _
+    gcongr
   · refine (add_le_add_right (h (unitInterval.fract_mem _) unitInterval.one_mem
       (fract_lt_one _).le) _).trans
       (le_trans ?_ <|
         add_le_add_right (h unitInterval.zero_mem (unitInterval.fract_mem _) (fract_nonneg _)) _)
     rw [φ.one, add_assoc, add_comm (1 : ℝ)]
-    refine add_le_add_left ?_ _
+    gcongr
     norm_cast
 
 protected theorem fract_fract (t : ℝ) : fract (φ (fract t)) = fract (φ t) := by
@@ -121,7 +121,7 @@ theorem linearReparam_monotone : Monotone linearReparam := by
     norm_num; linarith
   have : MonotoneOn linearReparam (Icc 4⁻¹ (3 / 4)) := fun x hx y hy hxy ↦ by
     rw [this x hx, this y hy]
-    exact sub_le_sub_right (mul_le_mul_of_nonneg_left hxy zero_le_two) _
+    gcongr
   have : MonotoneOn linearReparam (Icc 4⁻¹ 1) := fun x hx y hy hxy ↦ by
     obtain (h1y | h1y) := le_total y (3 / 4)
     · exact this ⟨hx.1, hxy.trans h1y⟩ ⟨hy.1, h1y⟩ hxy

SphereEversion/ToMathlib/Topology/Paracompact.lean

@@ -31,8 +31,8 @@ theorem exists_countable_locallyFinite_cover {ι X : Type*} [TopologicalSpace X]
     suffices {m | (U m ∩ U n).Nonempty} ⊆ Icc (n - 2) (n + 2) by exact (finite_Icc _ _).subset this
     rintro m ⟨x, ⟨⟨hx₁, hx₂⟩, ⟨hx₃, hx₄⟩⟩⟩
     simp only [mem_Icc, tsub_le_iff_right]
-    suffices ∀ {a b : ℕ}, x ∉ K a → x ∈ interior (K b.succ) → a ≤ b by
-      exact ⟨this hx₄ hx₁, this hx₂ hx₃⟩
+    suffices ∀ {a b : ℕ}, x ∉ K a → x ∈ interior (K b.succ) → a ≤ b from
+      ⟨this hx₄ hx₁, this hx₂ hx₃⟩
     intro a b ha hb
     by_contra hab
     replace hab : b + 1 ≤ a := by simpa using hab