chore: use grw, gcongr more (leanprover-community#30508)

Golf many proofs using `grw`, `gcongr`, `cutsat`, `linarith`... For this, tag a few more lemmas with `gcongr`, and make some existing ones stronger.

The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern.

The precise golfs that are performed are motivated by leanprover-community#30242, where four pairs of very basic and widespread lemmas get swapped. The best way to reduce the number of swaps needed is to simply not mention the lemmas explicitly.

Author: YaelDillies

Archive/Imo/Imo2001Q3.lean

@@ -87,8 +87,7 @@ lemma card_not_easy_le_210 (hG : ∀ i, #(G i) ≤ 6) (hB : ∀ i j, ¬Disjoint
       exact Nat.le_of_lt_succ mp.2
     _ ≤ ∑ i : Fin 21, 5 * 2 := by
       gcongr with i
-      rw [sum_const, smul_eq_mul]
-      exact mul_le_mul_right' (card_not_easy_le_five (hG _) (hB _)) _
+      grw [sum_const, smul_eq_mul, card_not_easy_le_five (hG _) (hB _)]
     _ = _ := by norm_num
 
 theorem result (h : Condition G B) : ∃ p, Easy G p ∧ Easy B p := by

Mathlib/Algebra/AddConstMap/Basic.lean

@@ -257,7 +257,7 @@ protected theorem rel_map_of_Icc [AddCommGroup G] [LinearOrder G] [IsOrderedAddM
       calc
         y ≤ l + a + n • a := sub_le_iff_le_add.1 hny.2
         _ = l + (n + 1) • a := by rw [add_comm n, add_smul, one_smul, add_assoc]
-        _ ≤ l + 0 • a := add_le_add_left (zsmul_le_zsmul_left ha.le (by cutsat)) _
+        _ ≤ l + (0 : ℤ) • a := by gcongr; cutsat
         _ ≤ x := by simpa using hx.1
     · -- If `n = 0`, then `l < y ≤ l + a`, hence we can apply the assumption
       exact hf x (Ico_subset_Icc_self hx) y (by simpa using Ioc_subset_Icc_self hny) hxy

Mathlib/Algebra/AlgebraicCard.lean

@@ -52,8 +52,7 @@ theorem cardinalMk_lift_le_mul :
 
 theorem cardinalMk_lift_le_max :
     Cardinal.lift.{u} #{ x : A // IsAlgebraic R x } ≤ max (Cardinal.lift.{v} #R) ℵ₀ :=
-  (cardinalMk_lift_le_mul R A).trans <|
-    (mul_le_mul_right' (lift_le.2 cardinalMk_le_max) _).trans <| by simp
+  (cardinalMk_lift_le_mul R A).trans <| by grw [lift_le.2 cardinalMk_le_max]; simp
 
 @[simp]
 theorem cardinalMk_lift_of_infinite [Infinite R] :

Mathlib/Algebra/MonoidAlgebra/Degree.lean

@@ -97,14 +97,15 @@ section AddOnly
 variable [Add A] [Add B] [Add T] [AddLeftMono B] [AddRightMono B]
   [AddLeftMono T] [AddRightMono T]
 
-theorem sup_support_mul_le {degb : A → B} (degbm : ∀ {a b}, degb (a + b) ≤ degb a + degb b)
+theorem sup_support_mul_le {degb : A → B} (degbm : ∀ a b, degb (a + b) ≤ degb a + degb b)
     (f g : R[A]) :
     (f * g).support.sup degb ≤ f.support.sup degb + g.support.sup degb := by
   classical
-  exact (Finset.sup_mono <| support_mul _ _).trans <| Finset.sup_add_le.2 fun _fd fds _gd gds ↦
-    degbm.trans <| add_le_add (Finset.le_sup fds) (Finset.le_sup gds)
+  grw [support_mul, Finset.sup_add_le]
+  rintro _fd fds _gd gds
+  grw [degbm, ← Finset.le_sup fds, ← Finset.le_sup gds]
 
-theorem le_inf_support_mul {degt : A → T} (degtm : ∀ {a b}, degt a + degt b ≤ degt (a + b))
+theorem le_inf_support_mul {degt : A → T} (degtm : ∀ a b, degt a + degt b ≤ degt (a + b))
     (f g : R[A]) :
     f.support.inf degt + g.support.inf degt ≤ (f * g).support.inf degt :=
   sup_support_mul_le (B := Tᵒᵈ) degtm f g
@@ -126,8 +127,7 @@ theorem sup_support_list_prod_le (degb0 : degb 0 ≤ 0)
     exact fun a ha => by rwa [Finset.mem_singleton.mp (Finsupp.support_single_subset ha)]
   | f::fs => by
     rw [List.prod_cons, List.map_cons, List.sum_cons]
-    exact (sup_support_mul_le (@fun a b => degbm a b) _ _).trans
-        (add_le_add_left (sup_support_list_prod_le degb0 degbm fs) _)
+    grw [sup_support_mul_le degbm, sup_support_list_prod_le degb0 degbm]
 
 theorem le_inf_support_list_prod (degt0 : 0 ≤ degt 0)
     (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (l : List R[A]) :

Mathlib/Algebra/MvPolynomial/Degrees.lean

@@ -402,7 +402,7 @@ theorem totalDegree_add_eq_right_of_totalDegree_lt {p q : MvPolynomial σ R}
 
 theorem totalDegree_mul (a b : MvPolynomial σ R) :
     (a * b).totalDegree ≤ a.totalDegree + b.totalDegree :=
-  sup_support_mul_le (by exact (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le) _ _
+  sup_support_mul_le (fun _ _ ↦ (Finsupp.sum_add_index' (fun _ => rfl) (fun _ _ _ => rfl)).le) _ _
 
 theorem totalDegree_smul_le [CommSemiring S] [DistribMulAction R S] (a : R) (f : MvPolynomial σ S) :
     (a • f).totalDegree ≤ f.totalDegree :=
@@ -434,8 +434,7 @@ theorem totalDegree_list_prod :
     ∀ s : List (MvPolynomial σ R), s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum
   | [] => by rw [List.prod_nil, totalDegree_one, List.map_nil, List.sum_nil]
   | p::ps => by
-    rw [List.prod_cons, List.map, List.sum_cons]
-    exact le_trans (totalDegree_mul _ _) (add_le_add_left (totalDegree_list_prod ps) _)
+    grw [List.prod_cons, List.map, List.sum_cons, totalDegree_mul, totalDegree_list_prod]
 
 theorem totalDegree_multiset_prod (s : Multiset (MvPolynomial σ R)) :
     s.prod.totalDegree ≤ (s.map MvPolynomial.totalDegree).sum := by

Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean

@@ -100,7 +100,7 @@ lemma schwartz_zippel_sup_sum :
         calc
           #{x ∈ S ^^ (n + 1) | eval x p = 0 ∧ eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0)
             ≤ #{x ∈ S ^^ (n + 1) | eval (tail x) pₖ = 0} / ∏ i, (#(S i) : ℚ≥0) := by
-            gcongr; exact fun x hx ↦ hx.2
+            gcongr with x; exact And.right
           _ = #(S 0) * #{xₜ ∈ tail S ^^ n | eval xₜ pₖ = 0}
               / (#(S 0) * (∏ i, #(S (.succ i)) : ℚ≥0)) := by
             rw [card_consEquiv_filter_piFinset S fun x ↦ eval x pₖ = 0, prod_univ_succ, tail_def]

Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

@@ -352,18 +352,13 @@ theorem card_le_card_biUnion {s : Finset ι} {f : ι → Finset α} (hs : (s : S
 theorem card_le_card_biUnion_add_card_fiber {s : Finset ι} {f : ι → Finset α}
     (hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + #{i ∈ s | f i = ∅} := by
   rw [← Finset.filter_card_add_filter_neg_card_eq_card fun i ↦ f i = ∅, add_comm]
-  exact
-    add_le_add_right
-      ((card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
-            nonempty_of_ne_empty <| (mem_filter.1 hi).2).trans <|
-        card_le_card <| biUnion_subset_biUnion_of_subset_left _ <| filter_subset _ _)
-      _
+  grw [card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
+    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset]
 
 theorem card_le_card_biUnion_add_one {s : Finset ι} {f : ι → Finset α} (hf : Injective f)
-    (hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + 1 :=
-  (card_le_card_biUnion_add_card_fiber hs).trans <|
-    add_le_add_left
-      (card_le_one.2 fun _ hi _ hj ↦ hf <| (mem_filter.1 hi).2.trans (mem_filter.1 hj).2.symm) _
+    (hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + 1 := by
+  grw [card_le_card_biUnion_add_card_fiber hs,
+    card_le_one.2 fun _ hi _ hj ↦ hf <| (mem_filter.1 hi).2.trans (mem_filter.1 hj).2.symm]
 
 end DoubleCounting
 

Mathlib/Algebra/Order/BigOperators/Group/List.lean

@@ -45,7 +45,7 @@ lemma Sublist.prod_le_prod' [Preorder M] [MulRightMono M]
     exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
   | cons₂ a _ ih' =>
     simp only [prod_cons, forall_mem_cons] at h₁ ⊢
-    exact mul_le_mul_left' (ih' h₁.2) _
+    grw [ih' h₁.2]
 
 @[to_additive sum_le_sum]
 lemma SublistForall₂.prod_le_prod' [Preorder M]

Mathlib/Algebra/Order/BigOperators/Group/Multiset.lean

@@ -89,8 +89,8 @@ lemma le_prod_of_submultiplicative_on_pred (f : α → β)
   intro a s hs hpsa
   have hps : ∀ x, x ∈ s → p x := fun x hx => hpsa x (mem_cons_of_mem hx)
   have hp_prod : p s.prod := prod_induction p s hp_mul hp_one hps
-  rw [prod_cons, map_cons, prod_cons]
-  exact (h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod).trans (mul_le_mul_left' (hs hps) _)
+  grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod,
+    hs hps]
 
 @[to_additive le_sum_of_subadditive]
 lemma le_prod_of_submultiplicative (f : α → β) (h_one : f 1 = 1)
@@ -112,7 +112,7 @@ lemma le_prod_nonempty_of_submultiplicative_on_pred (f : α → β) (p : α →
   have hsa_restrict : ∀ x, x ∈ s → p x := fun x hx => hsa_prop x (mem_cons_of_mem hx)
   have hp_sup : p s.prod := prod_induction_nonempty p hp_mul hs_empty hsa_restrict
   have hp_a : p a := hsa_prop a (mem_cons_self a s)
-  exact (h_mul a _ hp_a hp_sup).trans (mul_le_mul_left' (hs hs_empty hsa_restrict) _)
+  grw [h_mul a _ hp_a hp_sup, ← hs hs_empty hsa_restrict]
 
 @[to_additive le_sum_nonempty_of_subadditive]
 lemma le_prod_nonempty_of_submultiplicative (f : α → β) (h_mul : ∀ a b, f (a * b) ≤ f a * f b)

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -166,8 +166,7 @@ lemma prod_add_prod_le' (hi : i ∈ s) (h2i : g i + h i ≤ f i) (hgf : ∀ j 
     (hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j) : ((∏ i ∈ s, g i) + ∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i := by
   classical
   simp_rw [prod_eq_mul_prod_diff_singleton hi]
-  refine le_trans ?_ (mul_le_mul_right' h2i _)
-  rw [right_distrib]
+  grw [← h2i, right_distrib]
   gcongr with j hj j hj <;> simp_all
 
 end CanonicallyOrderedAdd