chore: golf using grw (#26981)

This PR cleans up some proofs using `grw`. It also tags a few lemmas with `@[gcongr]` that were required for the proofs.

Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>

Author: JovanGerb

Archive/Wiedijk100Theorems/CubingACube.lean

@@ -355,7 +355,7 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
   have hs : s.Nonempty := by
     rcases (nontrivial_bcubes h v).exists_ne i with ⟨i', hi', h2i'⟩
     exact ⟨i', hi', h2i'⟩
-  rcases Set.exists_min_image s (w ∘ cs) (Set.toFinite _) hs with ⟨i', ⟨hi', h2i'⟩, h3i'⟩
+  rcases Set.exists_min_image s (w <| cs ·) (Set.toFinite _) hs with ⟨i', ⟨hi', h2i'⟩, h3i'⟩
   rw [mem_singleton_iff] at h2i'
   let x := c.b j.succ + c.w - (cs i').w
   have hx : x < (cs i).b j.succ := by
@@ -368,8 +368,7 @@ theorem smallest_onBoundary {j} (bi : OnBoundary (mi_mem_bcubes : mi h v ∈ _)
   · simp only [side, not_and_or, not_lt, not_le, mem_Ico]; left; exact hx
   intro i'' hi'' h2i'' h3i''; constructor; swap; · apply lt_trans hx h3i''.2
   rw [le_sub_iff_add_le]
-  refine le_trans ?_ (t_le_t hi'' j); gcongr; apply h3i' i'' ⟨hi'', _⟩
-  simp [i, h2i'']
+  grw [← t_le_t hi'', h3i' i'' ⟨hi'', h2i''⟩]
 
 variable (h v)
 

Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

@@ -397,10 +397,9 @@ def freeMap {X Y : TopCat.{v}} (f : X ⟶ Y) : freeObj R X ⟶ freeObj R Y :=
     refine sInf_le ⟨continuousSMul_induced (Finsupp.lmapDomain _ _ f.hom),
       continuousAdd_induced (Finsupp.lmapDomain _ _ f.hom), ?_⟩
     rw [← coinduced_le_iff_le_induced]
-    refine le_trans ?_ hτ₃
-    refine le_of_eq_of_le ?_ (coinduced_mono (continuous_iff_coinduced_le.mp f.hom.2))
+    grw [← hτ₃, ← coinduced_mono (continuous_iff_coinduced_le.mp f.hom.2)]
     rw [coinduced_compose, coinduced_compose]
-    congr 1
+    congr! 1
     ext x
     simp [coe_freeObj]⟩
 

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -948,7 +948,8 @@ theorem normalClosure_eq_top_of {N : Subgroup G} [hn : N.Normal] {g g' : G} {hg
       MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]
     rw [mul_assoc, mul_inv_cancel, mul_one]
   rw [eq_top_iff, ← MonoidHom.range_eq_top.2 hs, MonoidHom.range_eq_map]
-  refine le_trans (map_mono (eq_top_iff.1 ht)) (map_le_iff_le_comap.2 (normalClosure_le_normal ?_))
+  grw [eq_top_iff.1 ht]
+  refine map_le_iff_le_comap.2 (normalClosure_le_normal ?_)
   rw [Set.singleton_subset_iff, SetLike.mem_coe]
   simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
     MonoidHom.restrict_apply, mem_comap]

Mathlib/Algebra/Lie/Engel.lean

@@ -119,9 +119,10 @@ theorem lcs_le_lcs_of_is_nilpotent_span_sup_eq_top {n i j : ℕ}
     refine ⟨(Submodule.map_mono ih).trans ?_, le_sup_of_le_right ?_⟩
     · rw [Submodule.map_sup, ← Submodule.map_comp, ← Module.End.mul_eq_comp, ← pow_succ', ←
         I.lcs_succ]
-      exact sup_le_sup_left coe_map_toEnd_le _
-    · refine le_trans (mono_lie_right I ?_) (mono_lie_right I hIM)
-      exact antitone_lowerCentralSeries R L M le_self_add
+      grw [coe_map_toEnd_le]
+    · norm_cast
+      gcongr
+      exact le_trans (antitone_lowerCentralSeries R L M le_self_add) hIM
 
 theorem isNilpotentOfIsNilpotentSpanSupEqTop (hnp : IsNilpotent <| toEnd R L M x)
     (hIM : IsNilpotent I M) : IsNilpotent L M := by

Mathlib/Algebra/Lie/IdealOperations.lean

@@ -153,6 +153,7 @@ theorem lie_eq_bot_iff : ⁅I, N⁆ = ⊥ ↔ ∀ x ∈ I, ∀ m ∈ N, ⁅(x :
   exact h x hx n hn
 
 variable {I J N N'} in
+@[gcongr]
 theorem mono_lie (h₁ : I ≤ J) (h₂ : N ≤ N') : ⁅I, N⁆ ≤ ⁅J, N'⁆ := by
   intro m h
   rw [lieIdeal_oper_eq_span, mem_lieSpan] at h; rw [lieIdeal_oper_eq_span, mem_lieSpan]

Mathlib/Algebra/Module/Submodule/IterateMapComap.lean

@@ -52,8 +52,8 @@ theorem iterateMapComap_le_succ (K : Submodule R N) (h : K.map f ≤ K.map i) (n
     simp_rw [iterateMapComap, iterate_succ', Function.comp_apply]
     calc
       _ ≤ (f.iterateMapComap i n K).map i := map_comap_le _ _
-      _ ≤ (((f.iterateMapComap i n K).map f).comap f).map i := map_mono (le_comap_map _ _)
-      _ ≤ _ := map_mono (comap_mono ih)
+      _ ≤ (((f.iterateMapComap i n K).map f).comap f).map i := by grw [← le_comap_map]
+      _ ≤ _ := by gcongr; exact ih
 
 /-- If `f` is surjective, `i` is injective, and there exists some `m` such that
 `LinearMap.iterateMapComap f i m K = LinearMap.iterateMapComap f i (m + 1) K`,

Mathlib/Algebra/Order/Archimedean/Basic.lean

@@ -415,7 +415,7 @@ theorem exists_div_btwn {x y : K} {n : ℕ} (h : x < y) (nh : (y - x)⁻¹ < n)
   rw [div_lt_iff₀ n0']
   refine ⟨(lt_div_iff₀ n0').2 <| (lt_iff_lt_of_le_iff_le (zh _)).1 (lt_add_one _), ?_⟩
   rw [Int.cast_add, Int.cast_one]
-  refine lt_of_le_of_lt (add_le_add_right ((zh _).1 le_rfl) _) ?_
+  grw [(zh _).1 le_rfl]
   rwa [← lt_sub_iff_add_lt', ← sub_mul, ← div_lt_iff₀' (sub_pos.2 h), one_div]
 
 theorem exists_rat_btwn {x y : K} (h : x < y) : ∃ q : ℚ, x < q ∧ q < y := by

Mathlib/Algebra/Order/CauSeq/BigOperators.lean

@@ -44,9 +44,8 @@ lemma of_abv_le (n : ℕ) (hm : ∀ m, n ≤ m → abv (f m) ≤ a m) :
   · simp [abv_zero abv]
   simp only [Nat.succ_add, Nat.succ_eq_add_one, Finset.sum_range_succ_comm]
   simp only [add_assoc, sub_eq_add_neg]
-  refine le_trans (abv_add _ _ _) ?_
   simp only [sub_eq_add_neg] at hi
-  exact add_le_add (hm _ (le_add_of_nonneg_of_le (Nat.zero_le _) (le_max_left _ _))) hi
+  grw [abv_add abv, hm _ (by omega), hi]
 
 lemma of_abv (hf : IsCauSeq abs fun m ↦ ∑ n ∈ range m, abv (f n)) :
     IsCauSeq abv fun m ↦ ∑ n ∈ range m, f n :=
@@ -127,7 +126,7 @@ theorem _root_.cauchy_product (ha : IsCauSeq abs fun m ↦ ∑ n ∈ range m, ab
         ∑ i ∈ range K with max N M + 1 ≤ i, abv (f i) * (2 * Q) := by
         gcongr
         rw [sub_eq_add_neg]
-        refine le_trans (abv_add _ _ _) ?_
+        grw [abv_add abv]
         rw [two_mul, abv_neg abv]
         gcongr <;> exact le_of_lt (hQ _)
     _ < ε / (4 * Q) * (2 * Q) := by

Mathlib/Algebra/Order/Field/Basic.lean

@@ -185,9 +185,9 @@ instance (priority := 100) LinearOrderedSemiField.toDenselyOrdered : DenselyOrde
     ⟨(a₁ + a₂) / 2,
       calc
         a₁ = (a₁ + a₁) / 2 := (add_self_div_two a₁).symm
-        _ < (a₁ + a₂) / 2 := div_lt_div_of_pos_right (add_lt_add_left h _) zero_lt_two,
+        _ < (a₁ + a₂) / 2 := by gcongr; exact zero_lt_two,
       calc
-        (a₁ + a₂) / 2 < (a₂ + a₂) / 2 := div_lt_div_of_pos_right (add_lt_add_right h _) zero_lt_two
+        (a₁ + a₂) / 2 < (a₂ + a₂) / 2 := by gcongr; exact zero_lt_two
         _ = a₂ := add_self_div_two a₂
         ⟩
 

Mathlib/Algebra/Order/Group/Multiset.lean

@@ -186,7 +186,7 @@ theorem le_smul_dedup [DecidableEq α] (s : Multiset α) : ∃ n : ℕ, s ≤ n
   ⟨(s.map fun a => count a s).fold max 0,
     le_iff_count.2 fun a => by
       rw [count_nsmul]; by_cases h : a ∈ s
-      · refine le_trans ?_ (Nat.mul_le_mul_left _ <| count_pos.2 <| mem_dedup.2 h)
+      · grw [← one_le_count_iff_mem.2 <| mem_dedup.2 h]
         have : count a s ≤ fold max 0 (map (fun a => count a s) (a ::ₘ erase s a)) := by
           simp
         rw [cons_erase h] at this