feat(GRewrite): new grw implementation

Mathlib.lean

@@ -7059,6 +7059,7 @@ public import Mathlib.Tactic.GCongr.ForwardAttr
 public import Mathlib.Tactic.GRewrite
 public import Mathlib.Tactic.GRewrite.Core
 public import Mathlib.Tactic.GRewrite.Elab
+public import Mathlib.Tactic.GRewrite.SinglePass
 public import Mathlib.Tactic.Generalize
 public import Mathlib.Tactic.GeneralizeProofs
 public import Mathlib.Tactic.Group

Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

@@ -175,6 +175,7 @@ theorem _root_.SubmonoidClass.finsuppProd_mem {S : Type*} [SetLike S N] [Submono
   prod_mem fun _i hi => h _ (Finsupp.mem_support_iff.mp hi)
 
 -- Note: Using `gcongr` since `congr` doesn't accept this lemma.
+set_option linter.gcongr.grw false in
 @[to_additive (attr := gcongr)]
 theorem prod_congr {f : α →₀ M} {g1 g2 : α → M → N} (h : ∀ x ∈ f.support, g1 x (f x) = g2 x (f x)) :
     f.prod g1 = f.prod g2 :=

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

@@ -391,11 +391,11 @@ 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.card_filter_add_card_filter_not fun i ↦ f i = ∅, add_comm]
   grw [card_le_card_biUnion (hs.subset <| filter_subset _ _) fun i hi ↦
-    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset]
+    nonempty_of_ne_empty (mem_filter.1 hi).2, filter_subset (f · ≠ ∅)]
 
 theorem card_le_card_biUnion_add_one {s : Finset ι} {f : ι → Finset α} (hf : Injective f)
     (hs : (s : Set ι).PairwiseDisjoint f) : #s ≤ #(s.biUnion f) + 1 := by
-  grw [card_le_card_biUnion_add_card_fiber hs,
+  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/CauSeq/BigOperators.lean

@@ -50,7 +50,7 @@ lemma of_abv_le (n : ℕ) (hm : ∀ m, n ≤ m → abv (f m) ≤ a m) :
     simp only [Nat.succ_add, Nat.succ_eq_add_one, Finset.sum_range_succ_comm]
     simp only [add_assoc, sub_eq_add_neg]
     simp only [sub_eq_add_neg] at hi
-    grw [abv_add abv, hm _ (by omega), 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 :=

Mathlib/Algebra/Order/Group/Int/Sum.lean

@@ -59,13 +59,13 @@ lemma sum_Ico_le_sum {s : Finset ℤ} {c : ℤ} (hs : ∀ x ∈ s, c ≤ x) :
   set r := Ico c (c + #s)
   calc
     _ ≤ ∑ x ∈ r ∩ s, x + #(r \ s) • (c + #s) := by
-      grw [← sum_inter_add_sum_diff r s, ← sum_le_card_nsmul _ _ _ fun x mx ↦ ?_]
-      rw [mem_sdiff, mem_Ico] at mx; exact mx.1.2.le
+      grw [← sum_inter_add_sum_diff r s, ← sum_le_card_nsmul _ _ _ ?_]
+      grind
     _ = ∑ x ∈ s ∩ r, x + #(s \ r) • (c + #s) := by
       rw [inter_comm, card_sdiff_comm]
       rw [Int.card_Ico, add_sub_cancel_left, Int.toNat_natCast]
     _ ≤ _ := by
-      grw [← sum_inter_add_sum_diff s r, card_nsmul_le_sum _ _ _ fun x mx ↦ ?_]
+      grw [← sum_inter_add_sum_diff s r, card_nsmul_le_sum _ _ _ ?_]
       grind
 
 /-- Sharp lower bound for the sum of a finset of integers that is bounded below, `range` version. -/

Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean

@@ -65,7 +65,7 @@ variable [LE α]
 -- Note: in this section, we use `@[gcongr high]` so that these lemmas have a higher priority than
 -- lemmas like `mul_le_mul_of_nonneg_left`, which have an extra side condition.
 
-@[to_additive (attr := gcongr high)]
+@[to_additive (attr := gcongr high - 1)]
 theorem mul_le_mul_right [MulLeftMono α] {b c : α} (bc : b ≤ c) (a : α) : a * b ≤ a * c :=
   CovariantClass.elim _ bc
 
@@ -78,7 +78,7 @@ theorem le_of_mul_le_mul_left' [MulLeftReflectLE α] {a b c : α}
     b ≤ c :=
   ContravariantClass.elim _ bc
 
-@[to_additive (attr := gcongr high)]
+@[to_additive (attr := gcongr high - 1)]
 theorem mul_le_mul_left [i : MulRightMono α] {b c : α} (bc : b ≤ c) (a : α) : b * a ≤ c * a :=
   i.elim a bc
 

Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean

@@ -124,7 +124,7 @@ lemma pow_le_pow_mul_of_sq_le_mul [MulLeftMono M] {a b : M} (hab : a ^ 2 ≤ b *
   | n + 2, _ => by
     calc
       a ^ (n + 2) = a ^ (n + 1) * a := by rw [pow_succ]
-      _ ≤ b ^ n * a * a := by grw [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
+      _ ≤ b ^ n * a * a := by grw' [pow_le_pow_mul_of_sq_le_mul hab (by lia)]; simp
       _ = b ^ n * a ^ 2 := by rw [mul_assoc, sq]
       _ ≤ b ^ n * (b * a) := by grw [hab]
       _ = b ^ (n + 1) * a := by rw [← mul_assoc, ← pow_succ]

Mathlib/Algebra/Order/Sub/Defs.lean

@@ -111,8 +111,8 @@ section Cov
 
 variable [AddLeftMono α]
 
-theorem tsub_le_tsub_left (h : a ≤ b) (c : α) : c - b ≤ c - a :=
-  tsub_le_iff_left.mpr <| le_add_tsub.trans <| by gcongr
+theorem tsub_le_tsub_left (h : a ≤ b) (c : α) : c - b ≤ c - a := by
+  grw [tsub_le_iff_left, ← h, ← le_add_tsub]
 
 @[gcongr] theorem tsub_le_tsub (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c :=
   (tsub_le_tsub_right hab _).trans <| tsub_le_tsub_left hcd _

Mathlib/Algebra/Order/ToIntervalMod.lean

@@ -865,7 +865,7 @@ private theorem toIxxMod_total' (a b c : α) :
   replace := min_le_of_add_le_two_nsmul this.le
   rw [min_le_iff] at this
   rw [toIxxMod_iff, toIxxMod_iff]
-  grw [← toIcoMod_le_toIocMod, ← toIcoMod_le_toIocMod] at this
+  grw [← toIcoMod_le_toIocMod] at this
   exact this
 
 private theorem toIxxMod_total (a b c : α) :

Mathlib/Analysis/Calculus/TangentCone/Basic.lean

@@ -43,7 +43,7 @@ theorem tangentConeAt_mono_field
   simp only [tangentConeAt_def, setOf_subset_setOf]
   refine fun y hy ↦ hy.mono ?_
   rw [← smul_one_smul (Filter 𝕜')]
-  grw [le_top (a := ⊤ • 1)]
+  grw' [le_top (a := ⊤ • 1)]
 
 theorem Filter.HasBasis.tangentConeAt_eq_biInter_closure {ι} {p : ι → Prop} {U : ι → Set E}
     (h : (𝓝 0).HasBasis p U) :

Mathlib/Analysis/Complex/Trigonometric.lean

@@ -555,7 +555,7 @@ theorem cos_bound {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖cos x - (1 - x ^ 2 / 2)‖
       simp
     _ ≤ ‖-x * I‖ ^ 4 * (Nat.succ 4 * (Nat.factorial 4 * (4 : ℕ) : ℝ)⁻¹) / 2 +
         ‖x * I‖ ^ 4 * (Nat.succ 4 * (Nat.factorial 4 * (4 : ℕ) : ℝ)⁻¹) / 2 := by
-      grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]
+      grw' [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]
     _ ≤ ‖x‖ ^ 4 * (5 / 96) := by norm_num
 
 theorem sin_bound {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖sin x - (x - x ^ 3 / 6)‖ ≤ ‖x‖ ^ 4 * (5 / 96) :=
@@ -571,7 +571,7 @@ theorem sin_bound {x : ℂ} (hx : ‖x‖ ≤ 1) : ‖sin x - (x - x ^ 3 / 6)‖
       simp
     _ ≤ ‖-x * I‖ ^ 4 * (Nat.succ 4 * (Nat.factorial 4 * (4 : ℕ) : ℝ)⁻¹) / 2 +
         ‖x * I‖ ^ 4 * (Nat.succ 4 * (Nat.factorial 4 * (4 : ℕ) : ℝ)⁻¹) / 2 := by
-      grw [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]
+      grw' [exp_bound (by simpa) (by simp), exp_bound (by simpa) (by simp)]
     _ ≤ ‖x‖ ^ 4 * (5 / 96) := by norm_num
 
 end Complex

Mathlib/Analysis/Convex/StrictCombination.lean

@@ -57,7 +57,7 @@ lemma StrictConvex.centerMass_mem_interior {s : Set V} {t : Finset ι} {w : ι 
         refine LT.lt.ne' ?_
         have hwi : 0 < w i := by grind
         grw [hwi]
-        simp only [lt_add_iff_pos_right, gt_iff_lt]
+        simp only [lt_add_iff_pos_right]
         exact (sum_nonneg hs₀).lt_of_ne' hsum_t
       simp only [hzi, ← add_smul, ← add_div, ne_eq, hwi, not_false_eq_true, div_self, one_smul]
       by_cases! hijt : ∃ i'' j'', i'' ∈ t ∧ j'' ∈ t ∧ z i'' ≠ z j'' ∧ w i'' ≠ 0 ∧ w j'' ≠ 0

Mathlib/Analysis/Distribution/Support.lean

@@ -131,6 +131,7 @@ theorem _root_.Filter.HasBasis.notMem_dsupport {ι : Sort*} {p : ι → Prop}
     x ∉ dsupport f ↔ ∃ i, p i ∧ IsVanishingOn f (s i) := by
   simp [hl.mem_dsupport]
 
+set_option linter.gcongr.grw false in
 @[gcongr]
 theorem dsupport_subset_dsupport
     (h : ∀ (s : Set α) (_ : IsOpen s), IsVanishingOn g s → IsVanishingOn f s) :

Mathlib/Analysis/LocallyConvex/Bounded.lean

@@ -274,9 +274,7 @@ theorem IsVonNBounded.closure [T1Space E] [RegularSpace E] [ContinuousConstSMul
   rcases exists_mem_nhds_isClosed_subset hV with ⟨W, hW₁, hW₂, hW₃⟩
   specialize ha hW₁
   filter_upwards [ha] with b ha'
-  grw [closure_mono ha', closure_smul₀ b]
-  apply smul_set_mono
-  grw [closure_subset_iff_isClosed.mpr hW₂, hW₃]
+  grw [ha', closure_smul₀ b, closure_subset_iff_isClosed.mpr hW₂, hW₃]
 
 variable [ContinuousSMul 𝕜 E]
 

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

@@ -241,8 +241,8 @@ theorem IsTheta.rpow (hf : 0 ≤ᶠ[l] f) (hg : 0 ≤ᶠ[l] g) (h : f =Θ[l] g)
     (fun x => f x ^ r) =Θ[l] fun x => g x ^ r := by
   wlog hr : r ≥ 0 with rpow_pos
   · rw [← isTheta_inv]
-    grw [← EventuallyEq.isTheta <| hf.mono fun x hfx ↦ Real.rpow_neg hfx r]
-    grw [← EventuallyEq.isTheta <| hg.mono fun x hgx ↦ Real.rpow_neg hgx r]
+    grw' [← EventuallyEq.isTheta <| hf.mono fun x hfx ↦ Real.rpow_neg hfx r]
+    grw' [← EventuallyEq.isTheta <| hg.mono fun x hgx ↦ Real.rpow_neg hgx r]
     exact rpow_pos hf hg h <| by linarith
   exact ⟨h.1.rpow hr hg, h.2.rpow hr hf⟩
 

Mathlib/Analysis/SpecialFunctions/Stirling.lean

@@ -122,7 +122,7 @@ theorem log_stirlingSeq_diff_le (n : ℕ) :
   rcases n with (_ | n)
   · suffices 0 ≤ Real.log (Real.exp 1 / Real.sqrt 2) by simpa
     apply Real.log_nonneg
-    grw [one_le_div (by positivity), Real.sqrt_le_left (by positivity), ← Real.add_one_le_exp]
+    grw' [one_le_div (by positivity), Real.sqrt_le_left (by positivity), ← Real.add_one_le_exp]
     norm_num
   set r := ((1 : ℝ) / (2 * (n + 1) + 1)) ^ 2 with hr
   have hr1 : r < 1 := by grw [hr, ← n.zero_le]; norm_num

Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

@@ -398,6 +398,7 @@ theorem bound (hN : 4096 ≤ N) : (N : ℝ) ^ (nValue N : ℝ)⁻¹ / exp 1 < dV
     · rw [mul_comm, ← div_div, div_sqrt, le_div_iff₀]
       · norm_num [le_sqrt_log hN]
       · norm_num1
+    swap
     · rw [cast_pos, lt_ceil, cast_zero, Real.sqrt_pos]
       refine log_pos ?_
       rw [one_lt_cast]

Mathlib/Combinatorics/Additive/SubsetSum.lean

@@ -98,7 +98,7 @@ theorem card_succ_choose_two_lt_card_subsetSum_of_pos (A_pos : ∀ x ∈ A, 0 <
   | empty => simp
   | insert a A A_lt_a ih =>
     have A_pos' : ∀ x ∈ A, 0 < x := fun x hx => A_pos x (mem_insert_of_mem hx)
-    grw [card_insert_of_notMem fun ha => (A_lt_a a ha).false, Nat.choose_succ_left _ _ (by lia),
+    grw' [card_insert_of_notMem fun ha => (A_lt_a a ha).false, Nat.choose_succ_left _ _ (by lia),
       Nat.choose_one_right, add_right_comm, add_assoc, Nat.add_one_le_iff.2 (ih A_pos')]
     exact card_add_card_subsetSum_lt_card_subsetSum_insert_max A_pos' A_lt_a <| A_pos a <|
       mem_insert_self a A

Mathlib/Combinatorics/Matroid/Rank/ENat.lean

@@ -322,7 +322,7 @@ lemma eRk_le_eRk_add_eRk_diff (M : Matroid α) (h : Y ⊆ X) :
 
 lemma eRk_union_le_encard_add_eRk (M : Matroid α) (X Y : Set α) :
     M.eRk (X ∪ Y) ≤ X.encard + M.eRk Y :=
-  (M.eRk_union_le_eRk_add_eRk X Y).trans <| by grw [M.eRk_le_encard]
+  (M.eRk_union_le_eRk_add_eRk X Y).trans <| by grw [← M.eRk_le_encard]
 
 lemma eRk_union_le_eRk_add_encard (M : Matroid α) (X Y : Set α) :
     M.eRk (X ∪ Y) ≤ M.eRk X + Y.encard :=

Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean

@@ -121,4 +121,4 @@ theorem IsUpperSet.le_card_inter_finset (h𝒜 : IsUpperSet (𝒜 : Set (Finset
     card_sdiff_of_subset inter_subset_right, sdiff_inter_self_right, sdiff_compl,
     _root_.inf_comm] at this
   · grw [inter_subset_right]
-  · grw [← Fintype.card_finset, card_le_univ]
+  · grw [← Fintype.card_finset, card_le_univ 𝒜]

Mathlib/Combinatorics/SimpleGraph/Clique.lean

@@ -403,6 +403,7 @@ theorem CliqueFree.mono (h : m ≤ n) : G.CliqueFree m → G.CliqueFree n := by
 theorem CliqueFree.anti (h : G ≤ H) : H.CliqueFree n → G.CliqueFree n :=
   forall_imp fun _ ↦ mt <| IsNClique.mono h
 
+set_option linter.gcongr.grw false in
 /-- If a graph is cliquefree, any graph that is contained in it is also cliquefree. -/
 @[gcongr]
 theorem CliqueFree.comap {H : SimpleGraph β} (hle : H ⊑ G) (h : G.CliqueFree n) :

Mathlib/Data/Finsupp/Order.lean

@@ -44,6 +44,7 @@ variable [Zero α]
 section OrderedAddCommMonoid
 variable [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ h₂ : ι → α → β}
 
+set_option linter.gcongr.grw false in
 @[gcongr]
 lemma sum_le_sum (h : ∀ i ∈ f.support, h₁ i (f i) ≤ h₂ i (f i)) : f.sum h₁ ≤ f.sum h₂ :=
   Finset.sum_le_sum h

Mathlib/Data/Int/LeastGreatest.lean

@@ -54,7 +54,7 @@ def leastOfBdd {P : ℤ → Prop} [DecidablePred P] (b : ℤ) (Hb : ∀ z : ℤ,
     match elt, le.dest (Hb _ Helt), Helt with
     | _, ⟨n, rfl⟩, Hn => ⟨n, Hn⟩
   ⟨b + (Nat.find EX : ℤ), Nat.find_spec EX, fun z h => by
-    obtain ⟨n, rfl⟩ := le.dest (Hb _ h); grw [Int.ofNat_le.2 <| Nat.find_min' EX h]⟩
+    obtain ⟨n, rfl⟩ := le.dest (Hb _ h); grw [Nat.find_min' EX h]⟩
 
 /-- `Int.leastOfBdd` is the least integer satisfying a predicate which is false for all `z : ℤ` with
 `z < b` for some fixed `b : ℤ`. -/

Mathlib/Data/Nat/Choose/Lucas.lean

@@ -106,7 +106,7 @@ alias lucas_theorem_nat := choose_modEq_prod_range_choose_nat
 Also see `choose_mul_mul_modEq_choose_nat` for the version with `MOD`. -/
 theorem choose_mul_mul_modEq_choose :
     choose (p * a) (p * b) ≡ choose a b [ZMOD p] := by
-  grw [choose_modEq_choose_mod_mul_choose_div]
+  nth_grw 1 [choose_modEq_choose_mod_mul_choose_div]
   simp [NeZero.pos, Int.ModEq.refl]
 
 /-- For primes `p`, `choose (p * a) (p * b)` is congruent to `choose a b` modulo `p`.

Mathlib/Geometry/Euclidean/Triangle.lean

@@ -164,14 +164,14 @@ theorem angle_eq_angle_add_add_angle_add (x : V) {y : V} (hy : y ≠ 0) :
   have : -1 < n := by
     replace h := h.ge
     contrapose! h
-    grw [h, neg_smul, one_smul, angle_le_pi, ← angle_nonneg, ← angle_nonneg]
+    grw [h, neg_smul, one_smul, angle_le_pi, ← angle_nonneg]
     linear_combination Real.pi_pos
   have : n < 1 := by
     replace h := h.le
     by_contra! hn
     grw [← hn, one_smul, ← angle_nonneg x y, zero_add, two_mul] at h
     have h' := h.trans_eq (add_comm _ _)
-    grw [angle_le_pi] at h' h
+    nth_grw 1 [angle_le_pi] at h' h
     rw [add_le_add_iff_left, (angle_le_pi _ _).ge_iff_eq, angle_comm, angle_eq_pi_iff] at h' h
     obtain ⟨hxy, r₁, r₁_pos, hr₁⟩ := h'
     obtain ⟨-, r₂, r₂_pos, hr₂⟩ := h

Mathlib/InformationTheory/Coding/KraftMcMillan.lean

@@ -154,7 +154,7 @@ public theorem kraft_mcmillan_inequality {S : Finset (List α)} [Fintype α] [No
   let K := ∑ w ∈ S, (1 / (Fintype.card α : ℝ)) ^ w.length
   let maxLen : ℕ := S.sup List.length
   have hAbs : |1 / K| < 1 := by
-    grw [abs_of_pos (by positivity), div_lt_one] <;> grind
+    grw' [abs_of_pos (by positivity), div_lt_one] <;> grind
   have : Tendsto (fun r : ℕ => r * maxLen / K ^ r) atTop (nhds 0) := by
     simpa [mul_left_comm, mul_div_assoc] using
       (tendsto_self_mul_const_pow_of_abs_lt_one hAbs).const_mul (maxLen : ℝ)

Mathlib/MeasureTheory/Function/AEEqFun.lean

@@ -239,7 +239,7 @@ theorem compQuasiMeasurePreserving_congr (g : β →ₘ[ν] γ) (hf : QuasiMeasu
     {f' : α → β} (hf' : Measurable f') (h : f =ᵐ[μ] f') :
     compQuasiMeasurePreserving g f hf = compQuasiMeasurePreserving g f' (hf.congr hf' h) := by
   ext
-  grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving, h]
+  grw [coeFn_compQuasiMeasurePreserving, h]
 
 @[simp]
 theorem compQuasiMeasurePreserving_id (g : β →ₘ[ν] γ) :
@@ -253,8 +253,7 @@ theorem compQuasiMeasurePreserving_comp {γ : Type*} {mγ : MeasurableSpace γ}
     compQuasiMeasurePreserving g (f ∘ f') (hf.comp hf') =
     compQuasiMeasurePreserving (compQuasiMeasurePreserving g f hf) f' hf' := by
   ext
-  grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving,
-    coeFn_compQuasiMeasurePreserving, comp_assoc]
+  grw [coeFn_compQuasiMeasurePreserving, coeFn_compQuasiMeasurePreserving, comp_assoc]
 
 theorem compQuasiMeasurePreserving_iterate (g : α →ₘ[μ] γ) {f : α → α}
     (hf : QuasiMeasurePreserving f μ μ) (n : ℕ) :

Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

@@ -222,8 +222,7 @@ theorem lpMeasSubgroupToLpTrim_add (hm : m ≤ m0) (f g : lpMeasSubgroup F m p 
   grw [Lp.coeFn_add]
   refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_
   · exact (Lp.stronglyMeasurable _).add (Lp.stronglyMeasurable _)
-  grw [lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq,
-    ← Lp.coeFn_add]
+  grw [lpMeasSubgroupToLpTrim_ae_eq, ← Lp.coeFn_add]
   rfl
 
 theorem lpMeasSubgroupToLpTrim_neg (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ) :
@@ -232,7 +231,7 @@ theorem lpMeasSubgroupToLpTrim_neg (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ)
   grw [Lp.coeFn_neg]
   refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _).neg
     ?_
-  grw [lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, ← Lp.coeFn_neg]
+  grw [lpMeasSubgroupToLpTrim_ae_eq, ← Lp.coeFn_neg]
   rfl
 
 theorem lpMeasSubgroupToLpTrim_sub (hm : m ≤ m0) (f g : lpMeasSubgroup F m p μ) :
@@ -249,7 +248,7 @@ theorem lpMeasToLpTrim_smul (hm : m ≤ m0) (c : 𝕜) (f : lpMeas F 𝕜 m p μ
   · exact (Lp.stronglyMeasurable _).const_smul c
   grw [lpMeasToLpTrim_ae_eq]
   push_cast
-  grw [Lp.coeFn_smul, lpMeasToLpTrim_ae_eq]
+  grw [Lp.coeFn_smul]
 
 /-- `lpMeasSubgroupToLpTrim` preserves the norm. -/
 theorem lpMeasSubgroupToLpTrim_norm_map [hp : Fact (1 ≤ p)] (hm : m ≤ m0)

Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean

@@ -94,21 +94,18 @@ theorem condExpIndL1Fin_add (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x y :
     condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm hs hμs y := by
   ext1
   unfold condExpIndL1Fin Integrable.toL1
-  grw [Lp.coeFn_add, MemLp.coeFn_toLp, MemLp.coeFn_toLp, MemLp.coeFn_toLp, condExpIndSMul_add,
-    Lp.coeFn_add]
+  grw [Lp.coeFn_add, MemLp.coeFn_toLp, condExpIndSMul_add, Lp.coeFn_add]
 
 theorem condExpIndL1Fin_smul (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : ℝ) (x : G) :
     condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x := by
   ext1
-  grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
-    condExpIndSMul_smul, Lp.coeFn_smul]
+  grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndSMul_smul, Lp.coeFn_smul]
 
 theorem condExpIndL1Fin_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (hs : MeasurableSet s)
     (hμs : μ s ≠ ∞) (c : 𝕜) (x : F) :
     condExpIndL1Fin hm hs hμs (c • x) = c • condExpIndL1Fin hm hs hμs x := by
   ext1
-  grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
-    condExpIndSMul_smul, Lp.coeFn_smul]
+  grw [Lp.coeFn_smul, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndSMul_smul, Lp.coeFn_smul]
 
 theorem norm_condExpIndL1Fin_le (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (x : G) :
     ‖condExpIndL1Fin hm hs hμs x‖ ≤ μ.real s * ‖x‖ := by
@@ -131,8 +128,7 @@ theorem condExpIndL1Fin_disjoint_union (hs : MeasurableSet s) (ht : MeasurableSe
       (lt_top_iff_ne_top.mpr (ENNReal.add_ne_top.mpr ⟨hμs, hμt⟩))).ne x =
     condExpIndL1Fin hm hs hμs x + condExpIndL1Fin hm ht hμt x := by
   ext1
-  grw [Lp.coeFn_add, condExpIndL1Fin_ae_eq_condExpIndSMul, condExpIndL1Fin_ae_eq_condExpIndSMul,
-    condExpIndL1Fin_ae_eq_condExpIndSMul]
+  grw [Lp.coeFn_add, condExpIndL1Fin_ae_eq_condExpIndSMul]
   rw [condExpIndSMul]
   rw [indicatorConstLp_disjoint_union hs ht hμs hμt hst (1 : ℝ)]
   rw [map_add]
@@ -248,8 +244,7 @@ theorem aestronglyMeasurable_condExpInd (hs : MeasurableSet s) (hμs : μ s ≠
 @[simp]
 theorem condExpInd_empty : condExpInd G hm μ ∅ = (0 : G →L[ℝ] α →₁[μ] G) := by
   ext x
-  grw [condExpInd_ae_eq_condExpIndSMul, condExpIndSMul_empty, zero_apply, Lp.coeFn_zero,
-    Lp.coeFn_zero]
+  grw [condExpInd_ae_eq_condExpIndSMul, condExpIndSMul_empty, zero_apply, Lp.coeFn_zero]
 
 theorem condExpInd_smul' [NormedSpace ℝ F] [SMulCommClass ℝ 𝕜 F] (c : 𝕜) (x : F) :
     condExpInd F hm μ s (c • x) = c • condExpInd F hm μ s x :=

Mathlib/MeasureTheory/Function/LpSpace/Basic.lean

@@ -763,18 +763,14 @@ theorem add_compLp (L L' : E →SL[σ] F) (f : Lp E p μ) :
     (L + L').compLp f = L.compLp f + L'.compLp f := by
   ext1
   grw [Lp.coeFn_add, coeFn_compLp']
-  refine
-    EventuallyEq.trans ?_ (EventuallyEq.fun_add (L.coeFn_compLp' f).symm (L'.coeFn_compLp' f).symm)
-  filter_upwards with x
-  rw [coe_add', Pi.add_def]
+  rfl
 
 theorem smul_compLp {𝕜''} [NormedRing 𝕜''] [Module 𝕜'' F] [IsBoundedSMul 𝕜'' F]
     [SMulCommClass 𝕜' 𝕜'' F] (c : 𝕜'') (L : E →SL[σ] F) (f : Lp E p μ) :
     (c • L).compLp f = c • L.compLp f := by
   ext1
   grw [Lp.coeFn_smul, coeFn_compLp']
-  refine (L.coeFn_compLp' f).mono fun x hx => ?_
-  rw [Pi.smul_apply, hx, coe_smul', Pi.smul_def]
+  rfl
 
 theorem norm_compLp_le (L : E →SL[σ] F) (f : Lp E p μ) : ‖L.compLp f‖ ≤ ‖L‖ * ‖f‖ :=
   LipschitzWith.norm_compLp_le _ _ _