diff --git a/Mathlib.lean b/Mathlib.lean index bb0500c55fd203..a2ea7fd9cca02a 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/Algebra/BigOperators/Finsupp/Basic.lean b/Mathlib/Algebra/BigOperators/Finsupp/Basic.lean index f95fc4d751a6e7..6ab1d90885352c 100644 --- a/Mathlib/Algebra/BigOperators/Finsupp/Basic.lean +++ b/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 := diff --git a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean index 8e0269652e8d94..2dda4d731830e5 100644 --- a/Mathlib/Algebra/Order/BigOperators/Group/Finset.lean +++ b/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 diff --git a/Mathlib/Algebra/Order/CauSeq/BigOperators.lean b/Mathlib/Algebra/Order/CauSeq/BigOperators.lean index a306a8d68de573..c5374ff17a6049 100644 --- a/Mathlib/Algebra/Order/CauSeq/BigOperators.lean +++ b/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 := diff --git a/Mathlib/Algebra/Order/Group/Int/Sum.lean b/Mathlib/Algebra/Order/Group/Int/Sum.lean index b325c6fd59c347..e7ddc1a6d4620c 100644 --- a/Mathlib/Algebra/Order/Group/Int/Sum.lean +++ b/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. -/ diff --git a/Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean b/Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean index bbd2372aab7fd6..9864ef27225ad2 100644 --- a/Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean +++ b/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 diff --git a/Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean b/Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean index 55e935ec1d5bf8..95feb7b71250fe 100644 --- a/Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean +++ b/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] diff --git a/Mathlib/Algebra/Order/Sub/Defs.lean b/Mathlib/Algebra/Order/Sub/Defs.lean index 81ecfd518209e4..2c87d45dff689c 100644 --- a/Mathlib/Algebra/Order/Sub/Defs.lean +++ b/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 _ diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean index 20794291bfb051..9ae0435c6ecb8e 100644 --- a/Mathlib/Algebra/Order/ToIntervalMod.lean +++ b/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 : α) : diff --git a/Mathlib/Analysis/Calculus/TangentCone/Basic.lean b/Mathlib/Analysis/Calculus/TangentCone/Basic.lean index 6b15b633c211e8..95a84d6b1ecfee 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/Basic.lean +++ b/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) : diff --git a/Mathlib/Analysis/Complex/Trigonometric.lean b/Mathlib/Analysis/Complex/Trigonometric.lean index a8957cd0c6c181..693dda57c37b54 100644 --- a/Mathlib/Analysis/Complex/Trigonometric.lean +++ b/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 diff --git a/Mathlib/Analysis/Convex/StrictCombination.lean b/Mathlib/Analysis/Convex/StrictCombination.lean index 50e507cd935ca1..de03d8b5b5026f 100644 --- a/Mathlib/Analysis/Convex/StrictCombination.lean +++ b/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 diff --git a/Mathlib/Analysis/Distribution/Support.lean b/Mathlib/Analysis/Distribution/Support.lean index 6e1d0e5107fd99..0c9ea5d0844930 100644 --- a/Mathlib/Analysis/Distribution/Support.lean +++ b/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) : diff --git a/Mathlib/Analysis/LocallyConvex/Bounded.lean b/Mathlib/Analysis/LocallyConvex/Bounded.lean index a09a73c1f99b3b..496f7cfcc07af1 100644 --- a/Mathlib/Analysis/LocallyConvex/Bounded.lean +++ b/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] diff --git a/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean b/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean index e18a4589bdd58f..8999f8f3ffc5e6 100644 --- a/Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean +++ b/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⟩ diff --git a/Mathlib/Analysis/SpecialFunctions/Stirling.lean b/Mathlib/Analysis/SpecialFunctions/Stirling.lean index c966bbaec1bf4b..a38f67fc5b0109 100644 --- a/Mathlib/Analysis/SpecialFunctions/Stirling.lean +++ b/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 diff --git a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean b/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean index d17244da0a84c2..6599ace30c78d2 100644 --- a/Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean +++ b/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] diff --git a/Mathlib/Combinatorics/Additive/SubsetSum.lean b/Mathlib/Combinatorics/Additive/SubsetSum.lean index 530007ec7ec027..af4a8173c27e19 100644 --- a/Mathlib/Combinatorics/Additive/SubsetSum.lean +++ b/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 diff --git a/Mathlib/Combinatorics/Matroid/Rank/ENat.lean b/Mathlib/Combinatorics/Matroid/Rank/ENat.lean index d8b78438078899..2b287a54fd69e8 100644 --- a/Mathlib/Combinatorics/Matroid/Rank/ENat.lean +++ b/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 := diff --git a/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean b/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean index 58c968fd0cf20f..7e894e81d09db5 100644 --- a/Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean +++ b/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 𝒜] diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean index 6d5c164b94a8c6..1c5d0072ad6c0e 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean +++ b/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) : diff --git a/Mathlib/Data/Finsupp/Order.lean b/Mathlib/Data/Finsupp/Order.lean index d25b0895a49189..c2cfa829ea02d1 100644 --- a/Mathlib/Data/Finsupp/Order.lean +++ b/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 diff --git a/Mathlib/Data/Int/LeastGreatest.lean b/Mathlib/Data/Int/LeastGreatest.lean index 3b26d8563d063f..c1d12ce4c2de1a 100644 --- a/Mathlib/Data/Int/LeastGreatest.lean +++ b/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 : ℤ`. -/ diff --git a/Mathlib/Data/Nat/Choose/Lucas.lean b/Mathlib/Data/Nat/Choose/Lucas.lean index d7ad9a22219a70..2686246f921ca5 100644 --- a/Mathlib/Data/Nat/Choose/Lucas.lean +++ 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`. diff --git a/Mathlib/Geometry/Euclidean/Triangle.lean b/Mathlib/Geometry/Euclidean/Triangle.lean index 6b989cbc41a5b0..8279c0d4793cb6 100644 --- a/Mathlib/Geometry/Euclidean/Triangle.lean +++ b/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 diff --git a/Mathlib/InformationTheory/Coding/KraftMcMillan.lean b/Mathlib/InformationTheory/Coding/KraftMcMillan.lean index d0e594ee4cf964..e2759886b7a4de 100644 --- a/Mathlib/InformationTheory/Coding/KraftMcMillan.lean +++ b/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 : ℝ) diff --git a/Mathlib/MeasureTheory/Function/AEEqFun.lean b/Mathlib/MeasureTheory/Function/AEEqFun.lean index 506c28877e204b..0ceeb0fa683881 100644 --- a/Mathlib/MeasureTheory/Function/AEEqFun.lean +++ b/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 : ℕ) : diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean index ea6a1aa4b8e502..b0bc000b3f2af7 100644 --- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean +++ b/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) diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean index b80b443991c68c..0d879ac44ca555 100644 --- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL1.lean +++ b/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 := diff --git a/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean b/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean index 155d4adbf97dc9..d17cebb303ab20 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace/Basic.lean +++ b/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 _ _ _ diff --git a/Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean b/Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean index d6ceb34e46b6bb..f3575980c24d73 100644 --- a/Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean +++ b/Mathlib/MeasureTheory/Function/LpSpace/Indicator.lean @@ -218,10 +218,7 @@ theorem indicatorConstLp_disjoint_union {s t : Set α} (hs : MeasurableSet s) (h indicatorConstLp p hs hμs c + indicatorConstLp p ht hμt c := by ext1 grw [Lp.coeFn_add, indicatorConstLp_coeFn] - refine - EventuallyEq.trans ?_ - (EventuallyEq.fun_add indicatorConstLp_coeFn.symm indicatorConstLp_coeFn.symm) - rw [Set.indicator_union_of_disjoint hst] + rw [Set.indicator_union_of_disjoint hst, Pi.add_def] end IndicatorConstLp diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean index 91bbff2ab208d1..8c4e245d7517e6 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFunc.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFunc.lean @@ -677,6 +677,7 @@ lemma mk_le_mk {f g : α → β} {hf hg hf' hg'} : mk f hf hf' ≤ mk g hg hg' lemma mk_lt_mk {f g : α → β} {hf hg hf' hg'} : mk f hf hf' < mk g hg hg' ↔ f < g := Iff.rfl open scoped Classical in +set_option linter.gcongr.grw false in @[gcongr] lemma piecewise_mono (hf : ∀ a ∈ s, f₁ a ≤ f₂ a) (hg : ∀ a ∉ s, g₁ a ≤ g₂ a) : piecewise s hs f₁ g₁ ≤ piecewise s hs f₂ g₂ := Set.piecewise_mono hf hg diff --git a/Mathlib/MeasureTheory/Integral/Average.lean b/Mathlib/MeasureTheory/Integral/Average.lean index e61404b8e9ff7d..c21d6fdb2eba97 100644 --- a/Mathlib/MeasureTheory/Integral/Average.lean +++ b/Mathlib/MeasureTheory/Integral/Average.lean @@ -236,11 +236,13 @@ theorem setLIntegral_setLAverage (μ : Measure α) [IsFiniteMeasure μ] (f : α ∫⁻ _x in s, ⨍⁻ a in s, f a ∂μ ∂μ = ∫⁻ x in s, f x ∂μ := lintegral_laverage _ _ +set_option linter.gcongr.grw false in @[gcongr] theorem laverage_mono_ae (h : ∀ᵐ a ∂μ, f a ≤ g a) : ⨍⁻ a, f a ∂μ ≤ ⨍⁻ a, g a ∂μ := lintegral_mono_ae <| h.filter_mono <| Measure.ae_mono' Measure.smul_absolutelyContinuous +set_option linter.gcongr.grw false in @[gcongr] theorem setLAverage_mono_ae (s : Set α) (h : ∀ᵐ a ∂μ, f a ≤ g a) : ⨍⁻ a in s, f a ∂μ ≤ ⨍⁻ a in s, g a ∂μ := diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean index 26eafc9bef4b49..39b92a191028ef 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean @@ -203,7 +203,7 @@ theorem AbsolutelyContinuousOnInterval.const_of_ae_hasDerivAt_zero {f : ℝ → have slope_bound := hu₁ z (by simp) |>.right |>.le have : 0 < z.val.2 - z.val.1 := by linarith [hu₁ z (by simp)] grw [← slope_bound] - simp only [dist_eq_norm, slope, vsub_eq_sub, sub_zero, ge_iff_le, g, mul_comm] + simp only [dist_eq_norm, slope, vsub_eq_sub, sub_zero, g, mul_comm] nth_rw 1 [← Real.norm_of_nonneg this.le] simp only [norm_smul, Real.norm_eq_abs, norm_inv] field_simp diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Slope.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Slope.lean index 46d5b21a34a21f..e6779fde30d9f0 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Slope.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Slope.lean @@ -65,14 +65,14 @@ theorem MonotoneOn.intervalIntegral_slope_le {f : ℝ → ℝ} {a b c : ℝ} (hf'.mono_set (by grind [uIcc])) (hf'.mono_set (by grind [uIcc]))] have fU : ∫ (x : ℝ) in b..b + c, f x ≤ c * f (b + c) := by - grw [intervalIntegral.integral_mono_on (g := fun _ ↦ f (b + c)) + grw' [intervalIntegral.integral_mono_on (g := fun _ ↦ f (b + c)) (by linarith) (hf'.mono_set (by grind [uIcc])) (by simp) (by intros; apply hf <;> grind [uIcc])] simp have fL : c * f a ≤ ∫ (x : ℝ) in a..a + c, f x := by - grw [← intervalIntegral.integral_mono_on (f := fun _ ↦ f a) + grw' [← intervalIntegral.integral_mono_on (f := fun _ ↦ f a) (by linarith) (by simp) (hf'.mono_set (by grind [uIcc])) diff --git a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean index 6d38a0dcdbd300..1829226375a1a2 100644 --- a/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean +++ b/Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean @@ -135,7 +135,7 @@ lemma ext_of_lintegral_prod_mul_prod_boundedContinuousFunction refine tendsto_lintegral_filter_of_dominated_convergence 1 (Eventually.of_forall <| by fun_prop) (Eventually.of_forall fun n ↦ ae_of_all _ fun ω ↦ ?_) (by simp) (ae_of_all _ this) - grw [Finset.prod_le_one (by simp), Finset.prod_le_one (by simp)] + grw' [Finset.prod_le_one (by simp), Finset.prod_le_one (by simp)] · simp · exact fun j _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (ht j) _ _ · exact fun i _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (hs i) _ _ @@ -146,7 +146,7 @@ lemma ext_of_lintegral_prod_mul_prod_boundedContinuousFunction refine tendsto_lintegral_filter_of_dominated_convergence 1 (Eventually.of_forall <| by fun_prop) (Eventually.of_forall fun _ ↦ ae_of_all _ fun _ ↦ ?_) (by simp) (ae_of_all _ this) - grw [Finset.prod_le_one (by simp), Finset.prod_le_one (by simp)] + grw' [Finset.prod_le_one (by simp), Finset.prod_le_one (by simp)] · simp · exact fun j _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (ht j) _ _ · exact fun i _ ↦ HasOuterApproxClosed.apprSeq_apply_le_one (hs i) _ _ diff --git a/Mathlib/MeasureTheory/Measure/IntegralCharFun.lean b/Mathlib/MeasureTheory/Measure/IntegralCharFun.lean index 30601049d7428c..63d8aedd3943c0 100644 --- a/Mathlib/MeasureTheory/Measure/IntegralCharFun.lean +++ b/Mathlib/MeasureTheory/Measure/IntegralCharFun.lean @@ -125,7 +125,7 @@ lemma measureReal_abs_gt_le_integral_charFun [IsProbabilityMeasure μ] (hr : 0 < refine (sinc_le_inv_abs hx_ne).trans ?_ exact (inv_le_inv₀ (by positivity) (by positivity)).mpr (le_of_lt hx) _ ≤ 2 * ∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ := by - grw [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_] + grw' [setIntegral_le_integral (by fun_prop) <| ae_of_all _ fun x ↦ ?_] simp only [Pi.zero_apply, sub_nonneg] exact sinc_le_one (2 * r⁻¹ * x) _ ≤ 2 * ‖∫ x, 1 - sinc (2 * r⁻¹ * x) ∂μ‖ := by diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean b/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean index 02a38ea4c86e21..1694e2ba14f397 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Misc.lean @@ -413,7 +413,7 @@ theorem sum_Ioc_mul_eq_sum_sum (f g : ArithmeticFunction R) (N : ℕ) : intro _ constructor · intro ⟨_, h⟩ - grw [← h, Nat.mul_div_cancel_left _ (by lia)] + grw' [← h, Nat.mul_div_cancel_left _ (by lia)] · intro hm grw [hm] simp [mul_div_le, div_le_self] diff --git a/Mathlib/NumberTheory/Chebyshev.lean b/Mathlib/NumberTheory/Chebyshev.lean index 199bd15c297f4a..499ce189f73df7 100644 --- a/Mathlib/NumberTheory/Chebyshev.lean +++ b/Mathlib/NumberTheory/Chebyshev.lean @@ -470,7 +470,7 @@ theorem eventually_primeCounting_le {ε : ℝ} (εpos : 0 < ε) : rw [primeCounting_eq_theta_div_log_add_integral hx, add_mul, add_div] have hl : 0 ≤ log x := by bound rw [norm_of_nonneg (show 0 ≤ x / log x by bound), ← mul_div_assoc] at hx2 - grw [theta_le_log4_mul_x (by linarith), ← hx2] + grw' [theta_le_log4_mul_x (by linarith), ← hx2] grind [le_norm_self] end PrimeCounting diff --git a/Mathlib/NumberTheory/Height/MvPolynomial.lean b/Mathlib/NumberTheory/Height/MvPolynomial.lean index 5aa10221e202b7..7ba9906bf1e568 100644 --- a/Mathlib/NumberTheory/Height/MvPolynomial.lean +++ b/Mathlib/NumberTheory/Height/MvPolynomial.lean @@ -72,7 +72,7 @@ lemma AbsoluteValue.iSup_abv_linearMap_apply_le (v : AbsoluteValue K ℝ) (A : refine ciSup_le fun j ↦ ?_ grw [v.sum_le] simp only [map_mul] - grw [Finset.sum_le_sum (g := fun _ ↦ (⨆ ji, v (A ji)) * ⨆ i, v (x i)) fun i _ ↦ ?h] + grw' [Finset.sum_le_sum (g := fun _ ↦ (⨆ ji, v (A ji)) * ⨆ i, v (x i)) fun i _ ↦ ?h] case h => dsimp only gcongr @@ -339,8 +339,7 @@ theorem mulHeight_eval_le {N : ℕ} {p : ι' → MvPolynomial ι K} (hp : ∀ i, · grw [(isNonarchimedean _ v.prop).eval_mvPolynomial_le (hp j) x] gcongr · exact HH₁ v.val - · grw [le_max_left (iSup ..) 1] - exact HH₂ (fun j ↦ max (⨆ s : (p j).support, v.val (coeff s.val (p j))) 1) j + · grw [← HH₂, ← le_max_left] · exact mul_nonneg (iSup_nonneg fun _ ↦ by positivity) <| by simp only [HH₁] /-- Let `K` be a field with an admissible family of absolute values (giving rise diff --git a/Mathlib/NumberTheory/ModularForms/Bounds.lean b/Mathlib/NumberTheory/ModularForms/Bounds.lean index cec8939dd30806..a7b59310befeb5 100644 --- a/Mathlib/NumberTheory/ModularForms/Bounds.lean +++ b/Mathlib/NumberTheory/ModularForms/Bounds.lean @@ -277,7 +277,7 @@ lemma qExpansion_coeff_isBigO_of_norm_isBigO {k : ℤ} {Γ : Subgroup (GL (Fin 2 rw [Real.norm_of_nonneg hh.le, Function.Periodic.norm_qParam, ← Real.exp_nat_mul] gcongr · simp [field] - · grw [hn' _ (by simp [← UpperHalfPlane.coe_im])] + · grw' [hn' _ (by simp [← UpperHalfPlane.coe_im])] simp [← UpperHalfPlane.coe_im, Real.rpow_neg_eq_inv_rpow, hne] refine (intervalIntegral.integral_mono (by positivity) ?_ ?_ this).trans (le_of_eq ?_) · apply Continuous.intervalIntegrable diff --git a/Mathlib/Order/Basic.lean b/Mathlib/Order/Basic.lean index 05f27f95cae3b1..43bbba219c6fc4 100644 --- a/Mathlib/Order/Basic.lean +++ b/Mathlib/Order/Basic.lean @@ -176,11 +176,26 @@ theorem le_imp_le_of_le_of_le (h₁ : c ≤ a) (h₂ : b ≤ d) : a ≤ b → c theorem lt_imp_lt_of_le_of_le (h₁ : c ≤ a) (h₂ : b ≤ d) : a < b → c < d := fun hab ↦ (h₁.trans_lt hab).trans_le h₂ +/-- monotonicity of `≤` with respect to `→` -/ +@[gcongr, to_dual self (reorder := a b, c d, h₁ h₂)] +theorem ge_imp_ge_of_le_of_le (h₁ : a ≤ c) (h₂ : d ≤ b) : a ≥ b → c ≥ d := + fun hab ↦ (h₂.trans hab).trans h₁ + +/-- monotonicity of `<` with respect to `→` -/ +@[gcongr, to_dual self (reorder := a b, c d, h₁ h₂)] +theorem gt_imp_gt_of_le_of_le (h₁ : a ≤ c) (h₂ : d ≤ b) : a > b → c > d := + fun hab ↦ (h₂.trans_lt hab).trans_le h₁ + namespace Mathlib.Tactic.GCongr +open Lean Meta /-- See if the term is `a < b` and the goal is `a ≤ b`. -/ @[gcongr_forward] meta def exactLeOfLt : ForwardExt where - eval h goal := do goal.assignIfDefEq (← Lean.Meta.mkAppM ``le_of_lt #[h]) + eval h goal := do + let le_of_lt := .const ``le_of_lt [← mkFreshLevelMVar] + let (mvars, _, _) ← forallMetaTelescope (← inferType le_of_lt) + mvars[4]!.mvarId!.assignIfDefEq h + goal.assignIfDefEq (mkAppN le_of_lt mvars) end Mathlib.Tactic.GCongr diff --git a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean index c16da11afcdc79..bdcf9c4f7430e9 100644 --- a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean +++ b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean @@ -53,7 +53,6 @@ section Pi variable {ι : Type*} [Fintype ι] [DecidableEq ι] {E : ι → Type*} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace ℝ (E i)] {L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] StrongDual ℝ (E i) →L[ℝ] ℝ} - /-- Given `L i : (E i)' × (E i)' → ℝ` a family of continuous bilinear forms, `diagonalStrongDualPi L` is the continuous bilinear form over `(Π i, E i)'` which maps `(x, y) : (Π i, E i)' × (Π i, E i)'` to @@ -74,8 +73,8 @@ def diagonalStrongDualPi (L : (i : ι) → StrongDual ℝ (E i) →L[ℝ] Strong simp only [LinearMap.mk₂_apply, g] grw [norm_sum_le, sum_mul, sum_mul] gcongr with i _ - grw [le_opNorm₂, opNorm_comp_le, opNorm_comp_le, norm_single_le_one] - simp + grw [le_opNorm₂] + gcongr <;> grw [opNorm_comp_le, norm_single_le_one, mul_one] lemma diagonalStrongDualPi_apply (x y : StrongDual ℝ (Π i, E i)) : diagonalStrongDualPi L x y = ∑ i, L i (x ∘L (.single ℝ E i)) (y ∘L (.single ℝ E i)) := rfl @@ -121,12 +120,12 @@ def diagonalStrongDualProd LinearMap.mkContinuous₂ g (‖L₁‖ + ‖L₂‖) <| by intro x y simp only [LinearMap.mk₂_apply, g] - grw [norm_add_le, add_mul, add_mul] + grw [norm_add_le, le_opNorm₂, add_mul, add_mul] gcongr - · grw [le_opNorm₂, opNorm_comp_le, opNorm_comp_le, norm_inl_le_one] - simp - · grw [le_opNorm₂, opNorm_comp_le, opNorm_comp_le, norm_inr_le_one] - simp + · grw [opNorm_comp_le, norm_inl_le_one, mul_one] + · grw [opNorm_comp_le, norm_inl_le_one, mul_one] + · grw [opNorm_comp_le, norm_inr_le_one, mul_one] + · grw [opNorm_comp_le, norm_inr_le_one, mul_one] lemma diagonalStrongDualProd_apply (x y : StrongDual ℝ (E × F)) : diagonalStrongDualProd L₁ L₂ x y = diff --git a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean index 351c7bb96a9ea4..948c3ef859f8ee 100644 --- a/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean +++ b/Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean @@ -269,7 +269,7 @@ lemma mul_iInf (I : Ideal A) {ι : Type*} [Nonempty ι] (J : ι → Ideal A) : refine (le_iInf fun i ↦ mul_mono_right (iInf_le _ _)).antisymm ?_ have H : ⨅ i, I * J i ≤ I := (iInf_le _ (Nonempty.some ‹_›)).trans mul_le_right obtain ⟨K, hK⟩ := dvd_iff_le.mpr H - grw [hK, le_iInf (a := K) fun i ↦ ?_] + grw' [hK, le_iInf (a := K) fun i ↦ ?_] rw [← mul_le_mul_iff_of_pos_left (a := I), ← hK] · exact iInf_le _ _ · exact bot_lt_iff_ne_bot.mpr hI diff --git a/Mathlib/RingTheory/PowerSeries/Substitution.lean b/Mathlib/RingTheory/PowerSeries/Substitution.lean index b7baebdf17e236..ef25d873723933 100644 --- a/Mathlib/RingTheory/PowerSeries/Substitution.lean +++ b/Mathlib/RingTheory/PowerSeries/Substitution.lean @@ -146,7 +146,7 @@ lemma HasSubst.eventually_coeff_pow_eq_zero {f : A⟦X⟧} (hf : HasSubst f) (n refine Filter.eventually_of_mem (Filter.Ici_mem_atTop (k * (n + 1))) fun m hm n' hn' ↦ coeff_of_lt_order _ ?_ obtain ⟨m, rfl⟩ := le_iff_exists_add.mp (Set.mem_Ici.mp hm) - grw [pow_add, ← order_mul_ge, pow_mul, ← le_order_pow_of_constantCoeff_eq_zero _ + grw' [pow_add, ← order_mul_ge, pow_mul, ← le_order_pow_of_constantCoeff_eq_zero _ (by rwa [map_pow]), ← _root_.le_add_right le_rfl, Nat.cast_lt] lia diff --git a/Mathlib/RingTheory/Unramified/LocalStructure.lean b/Mathlib/RingTheory/Unramified/LocalStructure.lean index 8addca99368585..1ea012051e6cc4 100644 --- a/Mathlib/RingTheory/Unramified/LocalStructure.lean +++ b/Mathlib/RingTheory/Unramified/LocalStructure.lean @@ -176,7 +176,7 @@ private lemma exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_ let q := minpoly R x ^ (p.natDegree + 2) + p refine ⟨q, ?_, by simpa [q], ?_⟩ · refine ((minpoly.monic hRx).pow _).add_of_left (degree_lt_degree ?_) - grw [natDegree_pow' (by simp [minpoly.monic hRx]), + grw' [natDegree_pow' (by simp [minpoly.monic hRx]), ← Nat.le_mul_of_pos_right _ (minpoly.natDegree_pos hRx)]; lia -- To show that `q'(x) ∉ Q`, we first show that `m` still divides `q` only once in `κ(P)[X]`. have ⟨w, h₁, h₂⟩ : ∃ w, q.map (algebraMap R _) = p.map (algebraMap R _) * w ∧ ¬ m ∣ w := by diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index fd49ff7fca8b5e..3e0f8f336e11a5 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -124,6 +124,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 diff --git a/Mathlib/Tactic/GCongr/Core.lean b/Mathlib/Tactic/GCongr/Core.lean index cb30835936d1b4..b88926cb57cc9d 100644 --- a/Mathlib/Tactic/GCongr/Core.lean +++ b/Mathlib/Tactic/GCongr/Core.lean @@ -144,6 +144,11 @@ public meta section namespace Mathlib.Tactic.GCongr open Lean Meta +/-- Linter for `@[gcongr]` lemmas that are not suitable for use in `grw`. -/ +register_option linter.gcongr.grw : Bool := { + defValue := true + descr := "Linter for `@[gcongr]` lemmas that are not suitable for use in `grw`" } + /-- `GCongrKey` is the key used in the hashmap for looking up `gcongr` lemmas. -/ structure GCongrKey where /-- The name of the relation. For example, `a + b ≤ a + c` has ``relName := `LE.le``. -/ @@ -158,6 +163,22 @@ deriving Inhabited, BEq instance : Ord GCongrKey where compare a b := a.1.quickCmp b.1 |>.then (a.2.quickCmp b.2) |>.then (compare a.3 b.3) +/-- The data for a "main" hypothesis of a `gcongr` lemma. +That is a hypothesis of the form `∀ xs, a xs' ~ b xs'` where `xs'` is a subset of `xs`, +and `a` and `b` form a "varying pair" in the conclusion of the `gcongr` lemma. -/ +structure GCongrHyp where + /-- Index of the left varying argument. -/ + lhsIdx : Nat + /-- Index of the right varying argument. -/ + rhsIdx : Nat + /-- Index of the hypothesis itself. -/ + hypIdx : Nat + /-- In `∀ xs, a xs' ~ b xs'`, for each `x` in `xs`, the position it appears in `xs'`. + This information is used to infer suitable names when introducing these variables. -/ + hypsPos : List (Option Nat) + /-- Whether the order of the two varying arguments is the opposite from in the conclusion. -/ + isContra : Bool + /-- Structure recording the data for a "generalized congruence" (`gcongr`) lemma. -/ structure GCongrLemma where /-- The key under which the lemma is stored. -/ @@ -165,10 +186,11 @@ structure GCongrLemma where /-- The name of the lemma. -/ declName : Name /-- `mainSubgoals` are the subgoals on which `gcongr` will be recursively called. They store + - the indices of the two compared variables - the index of the hypothesis - the number of parameters in the hypothesis - whether it is contravariant (i.e. switches the order of the two arguments) -/ - mainSubgoals : Array (Nat × Nat × Bool) + mainSubgoals : Array GCongrHyp /-- The number of arguments that `declName` takes when applying it. -/ numHyps : Nat /-- The given priority of the lemma, for example as `@[gcongr high]`. -/ @@ -177,6 +199,8 @@ structure GCongrLemma where This is used for sorting the lemmas. For example, `a + b ≤ a + c` has `numVarying := 1`. -/ numVarying : Nat + /-- Whether the lemma is suitable for use in `grw`. -/ + forGrw : Bool deriving Inhabited /-- A collection of `GCongrLemma`, to be stored in the environment extension. -/ @@ -255,50 +279,55 @@ def makeGCongrLemma (hyps : Array Expr) (target : Expr) (declName : Name) (prio for e1 in lhsArgs, e2 in rhsArgs do -- we call such a pair a "varying argument" pair if the LHS/RHS inputs are not defeq -- (and not proofs) - let isEq ← isDefEq e1 e2 <||> (isProof e1 <&&> isProof e2) - if !isEq then - -- verify that the "varying argument" pairs are free variables (after eta-reduction) - let .fvar e1 := e1.eta | fail "Not all varying arguments are free variables" - let .fvar e2 := e2.eta | fail "Not all varying arguments are free variables" - -- add such a pair to the `pairs` array - pairs := pairs.push (e1, e2) + if ← isDefEq e1 e2 <||> (isProof e1 <&&> isProof e2) then continue + let e1 := e1.eta; let e2 := e2.eta + -- verify that the "varying argument" pairs are free variables (after eta-reduction) + unless e1.isFVar && e2.isFVar do fail "Not all varying arguments are free variables" + if (← e1.fvarId!.getBinderInfo).isInstImplicit && + (← e2.fvarId!.getBinderInfo).isInstImplicit then + continue + -- add such a pair to the `pairs` array + pairs := pairs.push (e1, e2) let numVarying := pairs.size if numVarying = 0 then fail "LHS and RHS are the same" let mut mainSubgoals := #[] - let mut i := 0 -- iterate over antecedents `hyp` to the lemma - for hyp in hyps do - mainSubgoals ← forallTelescopeReducing (← inferType hyp) fun args hypTy => do + for hyp in hyps, hypIdx in 0...* do + match ← forallTelescopeReducing (← inferType hyp) fun xs hypTy => do -- pull out the conclusion `hypTy` of the antecedent, and check whether it is of the form -- `lhs₁ _ ... _ ≈ rhs₁ _ ... _` (for a possibly different relation `≈` than the relation -- `rel` above) - let hypTy ← whnf hypTy - let findPair (lhs rhs : FVarId) : Option Bool := - pairs.findSome? fun pair => - if (lhs, rhs) == pair then false else if (rhs, lhs) == pair then true else none - if let some (_, lhs₁, rhs₁) := getRel hypTy then - if let .fvar lhs₁ := lhs₁.getAppFn then - if let .fvar rhs₁ := rhs₁.getAppFn then - -- check whether `(lhs₁, rhs₁)` is in some order one of the "varying argument" pairs from - -- the conclusion to the lemma - if let some isContra := findPair lhs₁ rhs₁ then - -- if yes, record the index of this antecedent as a "main subgoal", together with the - -- index of the "varying argument" pair it corresponds to - return mainSubgoals.push (i, args.size, isContra) - else - -- now check whether `hypTy` is of the form `rhs₁ _ ... _`, - -- and whether the last hypothesis is of the form `lhs₁ _ ... _`. - if let .fvar rhs₁ := hypTy.getAppFn then - if let some lastFVar := args.back? then - if let .fvar lhs₁ := (← inferType lastFVar).getAppFn then - if let some isContra := findPair lhs₁ rhs₁ then - return mainSubgoals.push (i, args.size - 1, isContra) - return mainSubgoals - i := i + 1 + let findGoal (lhs rhs : Expr) (xs : Array Expr) := + lhs.withApp fun lhs lhsArgs => rhs.withApp fun rhs rhsArgs => do + guard <| lhsArgs.all xs.contains && lhsArgs == rhsArgs + let lhsIdx ← hyps.idxOf? lhs + let rhsIdx ← hyps.idxOf? rhs + -- check whether `(lhs, rhs)` is in some order one of the "varying argument" pairs from + -- the conclusion to the lemma + let (pair, isContra) ← pairs.findSome? fun pair => + if (lhs, rhs) == pair then some (pair, false) else + if (rhs, lhs) == pair then some (pair, true) else none + let hypsPos := xs.toList.map lhsArgs.idxOf? + some ({ lhsIdx, rhsIdx, hypIdx, hypsPos, isContra }, pair) + if let some (_, lhs₁, rhs₁) := getRel (← whnf hypTy) then + return findGoal lhs₁ rhs₁ xs + else if let some lastFVar := xs.back? then + return findGoal (← inferType lastFVar) hypTy xs.pop + return none + with + | none => pure () + | some (mainSubgoal, pair) => + mainSubgoals := mainSubgoals.push mainSubgoal + pairs := pairs.erase pair + let forGrw := pairs.isEmpty + unless forGrw do + Linter.logLintIf linter.gcongr.grw (← getRef) + m!"Not all varying arguments have a corresponding hypothesis. \ + This means that the lemma cannot be used in `grw`." -- store all the information from this parse of the lemma's structure in a `GCongrLemma` let key := { relName, head, arity := lhsArgs.size } - return { key, declName, mainSubgoals, numHyps := hyps.size, prio, numVarying } + return { key, declName, mainSubgoals, numHyps := hyps.size, prio, numVarying, forGrw } /-- Attribute marking "generalized congruence" (`gcongr`) lemmas. Such lemmas must have a @@ -400,6 +429,16 @@ initialize registerBuiltinAttribute { initialize registerTraceClass `Meta.gcongr +def _root_.Lean.MVarId.applyRflOrId (goal : MVarId) : MetaM Unit := goal.withContext do + let t ← whnfR (← goal.getType) + if t.isForall then + let lhs := t.bindingDomain! + let rhs := t.bindingBody! + guard !rhs.hasLooseBVars + guard <| ← isDefEq lhs rhs + goal.assign (.lam t.bindingName! lhs (.bvar 0) t.bindingInfo!) + else + goal.applyRfl /-- `gcongr_discharger` is used by `gcongr` to discharge side goals. This is an extensible tactic using [`macro_rules`](lean-manual://section/tactic-macro-extension). @@ -510,49 +549,13 @@ For example, the relation `a ≡ b [ZMOD n]` has an instance of `IsTrans`, so a def relImpRelLemma (arity : Nat) : List GCongrLemma := if arity < 2 then [] else [{ declName := ``rel_imp_rel - mainSubgoals := #[(7, 0, true), (8, 0, false)] + mainSubgoals := #[⟨5, 3, 7, [], true⟩, ⟨4, 6, 8, [], false⟩] numHyps := 9 - key := default, prio := default, numVarying := default + key := default, prio := default, numVarying := default, forGrw := true }] end Trans -/-- -`Lean.MVarId.applyWithArity` is a copy of `Lean.MVarId.apply`, where the arity of the -applied function is given explicitly instead of being inferred. - -TODO: make `Lean.MVarId.apply` take a configuration argument to do this itself --/ -def _root_.Lean.MVarId.applyWithArity (mvarId : MVarId) (e : Expr) (arity : Nat) - (cfg : ApplyConfig := {}) (term? : Option MessageData := none) : MetaM (List MVarId) := - mvarId.withContext do - mvarId.checkNotAssigned `apply - let targetType ← mvarId.getType - let eType ← inferType e - let (newMVars, binderInfos) ← do - -- we use `withDefault` so that we can unfold `Monotone` - let (newMVars, binderInfos, eType) ← withDefault <| forallMetaTelescopeReducing eType arity - if (← isDefEqApply cfg.approx eType targetType) then - pure (newMVars, binderInfos) - else - let conclusionType? ← if arity = 0 then - pure none - else - let (_, _, r) ← withDefault <| forallMetaTelescopeReducing eType arity - pure (some r) - throwApplyError mvarId eType conclusionType? targetType term? - postprocessAppMVars `apply mvarId newMVars binderInfos - cfg.synthAssignedInstances cfg.allowSynthFailures - let e ← instantiateMVars e - mvarId.assign (mkAppN e newMVars) - let newMVars ← newMVars.filterM fun mvar => not <$> mvar.mvarId!.isAssigned - let otherMVarIds ← getMVarsNoDelayed e - let newMVarIds ← reorderGoals newMVars cfg.newGoals - let otherMVarIds := otherMVarIds.filter fun mvarId => !newMVarIds.contains mvarId - let result := newMVarIds ++ otherMVarIds.toList - result.forM (·.headBetaType) - return result - /-- The state used by `GCongrM`. -/ structure State where /-- The new goals produced by `gcongr`. This includes side-goals and main goals. @@ -581,25 +584,55 @@ def GCongrM.run {α} (x : GCongrM α) (patterns : List (TSyntax `rintroPat) := [ return (a, s.newGoals) /-- Add an unsolved goal to the `newGoals` array in the state. -/ -private def pushNewGoal (g : MVarId) : GCongrM Unit := +def pushNewGoal (g : MVarId) : GCongrM Unit := modify fun s ↦ { s with newGoals := s.newGoals.push g} /-- Run the `intro` tactic `n` times on the given goal. -/ -private def introN (goal : MVarId) (n : Nat) : GCongrM (List MVarId) := do +private def introN (goal : MVarId) (n : Nat) : GCongrM (Array MVarId) := do let (goals, patterns) ← goal.rintroWithPats (← get).patterns n modify ({· with patterns}) - return goals + return goals.toArray /-- Run the discharger for main goals. -/ private def dischargeMain (mvarId : MVarId) : GCongrM Bool := do (← read).mainGoalDischarger mvarId /-- Run the discharger for side goals. -/ -private def dischargeSide (mvarId : MVarId) : GCongrM Unit := do +def dischargeSide (mvarId : MVarId) : GCongrM Unit := do let mctx ← getMCtx try (← read).sideGoalDischarger (← mvarId.intros).2 catch _ => setMCtx mctx; pushNewGoal mvarId +def applyGCongrLemma (g : MVarId) (lem : GCongr.GCongrLemma) : + GCongrM (Array (MVarId × Bool) × Array MVarId) := do + let const ← mkConstWithFreshMVarLevels lem.declName + let type ← inferType const + -- we use `withDefault` so that we can unfold `Monotone` + let (mvars, _, type) ← withDefault <| forallMetaTelescopeReducing type lem.numHyps + guard <| ← approxDefEq <| isDefEq (← g.getType) type + g.assign (mkAppN const mvars) + let mut sideGoals := #[] + for mvar in mvars, i in 0...* do + unless ← mvar.mvarId!.isAssigned do + unless lem.mainSubgoals.any (fun h ↦ h.lhsIdx == i || h.rhsIdx == i || h.hypIdx == i) do + sideGoals := sideGoals.push mvar.mvarId! + let mainGoals ← lem.mainSubgoals.flatMapM fun h ↦ do + if (← get).patterns.isEmpty then + let lhsNames := lambdaBinderNames (← instantiateMVars mvars[h.lhsIdx]!) + let rhsNames := lambdaBinderNames (← instantiateMVars mvars[h.rhsIdx]!) + let lambdaNames := if lhsNames.size ≥ rhsNames.size then lhsNames else rhsNames + let names := h.hypsPos.map fun | some n => lambdaNames.getD n `_ | none => `_ + let mvarId := (← mvars[h.hypIdx]!.mvarId!.introN h.hypsPos.length names).2 + return #[(mvarId, h.isContra)] + else + return (← introN mvars[h.hypIdx]!.mvarId! h.hypsPos.length).map (·, h.isContra) + return (mainGoals, sideGoals) +where + lambdaBinderNames (e : Expr) (acc : Array Name := #[]) : Array Name := + match e with + | .lam n _ b _ => lambdaBinderNames b (acc.push n) + | _ => acc + /-- The core of the `gcongr` tactic. Parse a goal into the form `(f _ ... _) ∼ (f _ ... _)`, look up any relevant `@[gcongr]` lemmas, try to apply them, recursively run the tactic itself on "main" goals which are generated, and run the discharger on side goals which are generated. If there @@ -613,7 +646,7 @@ partial def _root_.Lean.MVarId.gcongr if mdataLhs?.isNone then -- A. If there is no pattern annotation, try to resolve the goal by reflexivity, or -- by the provided tactic `mainGoalDischarger`, and continue on if this fails. - try withReducible g.applyRfl; return true + try withReducible g.applyRflOrId; return true catch _ => if ← dischargeMain g then return true @@ -637,7 +670,7 @@ partial def _root_.Lean.MVarId.gcongr -- If there are no annotations at all, we close the goal with `rfl`. Otherwise, -- we report that the provided pattern doesn't apply. unless containsHoleAnnotation mdataExpr do - try withDefault g.applyRfl; return true + try withDefault g.applyRflOrId; return true catch _ => throwTacticEx `gcongr g m!"\ subgoal {← withReducible g.getType'} is not allowed by the provided pattern \ and is not closed by `rfl`" @@ -658,37 +691,27 @@ partial def _root_.Lean.MVarId.gcongr -- Look up the `@[gcongr]` lemmas whose conclusion has the same relation and head function as -- the goal let key := { relName, head := lhsHead, arity := lhsArgs.size } - let mut lemmas := (gcongrExt.getState (← getEnv)).getD key [] - if relName == `_Implies then - lemmas := lemmas ++ relImpRelLemma lhsArgs.size + let lemmas := ((gcongrExt.getState (← getEnv)).get? key).getD (relImpRelLemma lhsArgs.size) for lem in lemmas do - let gs ← try + try -- Try `apply`-ing such a lemma to the goal. - let const ← mkConstWithFreshMVarLevels lem.declName - withReducible (g.applyWithArity const lem.numHyps { synthAssignedInstances := false }) + let (mainGoals, sideGoals) ← withReducible (applyGCongrLemma g lem) + -- Try the discharger on any side goals which were not resolved by the `apply`. + for mvarId in sideGoals do + let type ← mvarId.getType + if (← isClass? type).isSome then + let some inst ← synthInstance? type | failure + guard <| ← isDefEq (.mvar mvarId) inst + else + dischargeSide mvarId + for (mvarId, isContra) in mainGoals do + -- Recurse: call ourself (`Lean.MVarId.gcongr`) on the subgoal + let mdataLhs?' := mdataLhs?.map (· != isContra) + discard <| mvarId.gcongr mdataLhs?' depth + return true catch _ => setMCtx mctx continue - let some e ← getExprMVarAssignment? g | panic! "unassigned?" - let args := e.getAppArgs - -- Map over the lemma's `mainSubgoals` list to find the recursive `gcongr` goals. - let mainSubgoals := lem.mainSubgoals.map fun (i, numHyps, isContra) ↦ - -- We anticipate that such a "main" subgoal should not have been solved by the `apply` by - -- unification ... - if let some (.mvar mvarId) := args[i]? then - (mvarId, numHyps, isContra) - else - panic! "what kind of lemma is this?" - -- Try the discharger on any side goals which were not resolved by the `apply`. - for g in gs do - if !(← g.isAssigned) && !mainSubgoals.any (·.1 == g) then - dischargeSide g - for (mvarId, numHyps, isContra) in mainSubgoals do - let mdataLhs?' := mdataLhs?.map (· != isContra) - for mvarId in ← introN mvarId numHyps do - -- Recurse: call ourself (`Lean.MVarId.gcongr`) on the subgoal - discard <| mvarId.gcongr mdataLhs?' depth - return true -- A. If there is no template, and there was no `@[gcongr]` lemma which matched the goal, -- report this goal back. if mdataLhs?.isNone then diff --git a/Mathlib/Tactic/GCongr/CoreAttrs.lean b/Mathlib/Tactic/GCongr/CoreAttrs.lean index e6064ffa448cfa..0f9910640133f9 100644 --- a/Mathlib/Tactic/GCongr/CoreAttrs.lean +++ b/Mathlib/Tactic/GCongr/CoreAttrs.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2024 Yury Kudryashov. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Yury Kudryashov +Authors: Yury Kudryashov, Jovan Gerbscheid -/ module @@ -18,24 +18,17 @@ public meta section namespace Mathlib.Tactic.GCongr -variable {a b c : Prop} +variable {a b c d : Prop} -lemma imp_trans (h : a → b) : (b → c) → a → c := fun g ha => g (h ha) +lemma imp_mono (h₁ : c → a) (h₂ : c → b → d) : (a → b) → c → d := + fun h₃ hc => h₂ hc (h₃ (h₁ hc)) -lemma imp_right_mono (h : a → b → c) : (a → b) → a → c := - fun h' ha => h ha (h' ha) +lemma and_mono (h₁ : a → c) (h₂ : a → b → d) : (a ∧ b) → c ∧ d := + fun ⟨ha, hb⟩ => ⟨h₁ ha, h₂ ha hb⟩ -lemma and_right_mono (h : a → b → c) : (a ∧ b) → a ∧ c := - fun ⟨ha, hb⟩ => ⟨ha, h ha hb⟩ - -attribute [gcongr] mt - Or.imp Or.imp_left Or.imp_right - And.imp And.imp_left GCongr.and_right_mono - imp_imp_imp GCongr.imp_trans GCongr.imp_right_mono - forall_imp Exists.imp - List.Sublist.append List.Sublist.append_left List.Sublist.append_right - List.Sublist.reverse List.drop_sublist_drop_left List.Sublist.drop - List.Perm.cons List.Perm.append_left List.Perm.append_right List.Perm.append List.Perm.map +attribute [gcongr] mt Or.imp and_mono imp_mono forall_imp Exists.imp + List.Sublist.append List.Sublist.reverse List.drop_sublist_drop_left List.Sublist.drop + List.Perm.cons List.Perm.append List.Perm.map List.cons_subset_cons Nat.sub_le_sub_left Nat.sub_le_sub_right Nat.sub_lt_sub_left Nat.sub_lt_sub_right diff --git a/Mathlib/Tactic/GRewrite/Core.lean b/Mathlib/Tactic/GRewrite/Core.lean index 55b1b08da1825f..911888e2529887 100644 --- a/Mathlib/Tactic/GRewrite/Core.lean +++ b/Mathlib/Tactic/GRewrite/Core.lean @@ -68,7 +68,7 @@ If `symm = false`, we rewrite `e` to `eNew := e[x/y]`; otherwise `eNew := e[y/x] The code aligns with `Lean.MVarId.rewrite` as much as possible. -/ -def _root_.Lean.MVarId.grewrite (goal : MVarId) (e : Expr) (hrel : Expr) +def _root_.Lean.MVarId.grewrite' (goal : MVarId) (e : Expr) (hrel : Expr) (forwardImp symm : Bool) (config : GRewrite.Config) : MetaM GRewriteResult := goal.withContext do goal.checkNotAssigned `grewrite diff --git a/Mathlib/Tactic/GRewrite/Elab.lean b/Mathlib/Tactic/GRewrite/Elab.lean index 0743e0cf2ae12d..08079bb3229668 100644 --- a/Mathlib/Tactic/GRewrite/Elab.lean +++ b/Mathlib/Tactic/GRewrite/Elab.lean @@ -7,6 +7,7 @@ module public meta import Lean.Elab.Tactic.Rewrite public import Mathlib.Tactic.GRewrite.Core +public import Mathlib.Tactic.GRewrite.SinglePass /-! @@ -21,14 +22,14 @@ This file defines the tactics that use the backend defined in `Mathlib.Tactic.GR -/ -public meta section +meta section -namespace Mathlib.Tactic +namespace Mathlib.Tactic.GRewrite open Lean Meta Elab Parser Tactic /-- Apply the `grewrite` tactic to the current goal. -/ -def grewriteTarget (stx : Syntax) (symm : Bool) (config : GRewrite.Config) : TacticM Unit := do +def grewriteTarget' (stx : Syntax) (symm : Bool) (config : GRewrite.Config) : TacticM Unit := do let goal ← getMainGoal Term.withSynthesize <| goal.withContext do let e ← elabTerm stx none true @@ -36,13 +37,13 @@ def grewriteTarget (stx : Syntax) (symm : Bool) (config : GRewrite.Config) : Tac throwAbortTactic let goal ← getMainGoal let target ← goal.getType - let r ← goal.grewrite target e (forwardImp := false) (symm := symm) (config := config) + let r ← goal.grewrite' target e (forwardImp := false) (symm := symm) (config := config) let mvarNew ← mkFreshExprSyntheticOpaqueMVar r.eNew (← goal.getTag) goal.assign (mkApp r.impProof mvarNew) replaceMainGoal (mvarNew.mvarId! :: r.mvarIds) /-- Apply the `grewrite` tactic to a local hypothesis. -/ -def grewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : GRewrite.Config) : +def grewriteLocalDecl' (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : GRewrite.Config) : TacticM Unit := withMainContext do -- Note: we cannot execute `replace` inside `Term.withSynthesize`. -- See issues https://github.com/leanprover-community/mathlib4/issues/2711 and https://github.com/leanprover-community/mathlib4/issues/2727. @@ -52,11 +53,32 @@ def grewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : G if e.hasSyntheticSorry then throwAbortTactic let localDecl ← fvarId.getDecl - goal.grewrite localDecl.type e (forwardImp := true) (symm := symm) (config := config) + goal.grewrite' localDecl.type e (forwardImp := true) (symm := symm) (config := config) let proof := .app (r.impProof) (.fvar fvarId) let { mvarId, .. } ← goal.replace fvarId proof r.eNew replaceMainGoal (mvarId :: r.mvarIds) +/-- Apply the `grewrite` tactic to the current goal. -/ +def grewriteTarget (stx : Syntax) (symm : Bool) (config : Config) : TacticM Unit := do + let goal ← getMainGoal + goal.withContext do + let target ← goal.getType + let r ← elabGRewrite goal target stx (forwardImp := false) (symm := symm) (config := config) + let mvarNew ← mkFreshExprSyntheticOpaqueMVar r.eNew (← goal.getTag) + goal.assign (mkApp r.impProof mvarNew) + replaceMainGoal (mvarNew.mvarId! :: r.mvarIds) + +/-- Apply the `grewrite` tactic to a local hypothesis. -/ +def grewriteLocalDecl (stx : Syntax) (symm : Bool) (fvarId : FVarId) (config : Config) : + TacticM Unit := withMainContext do + let goal ← getMainGoal + let type ← fvarId.getType + let r ← elabGRewrite goal type stx (forwardImp := true) (symm := symm) (config := config) + let proof := .app (r.impProof) (.fvar fvarId) + let { mvarId, .. } ← goal.replace fvarId proof r.eNew + replaceMainGoal (mvarId :: r.mvarIds) + + /-- Function elaborating `GRewrite.Config`. -/ declare_config_elab elabGRewriteConfig GRewrite.Config @@ -95,7 +117,8 @@ interprets `· → ·` as a relation instead of adding the hypothesis as a side -/ syntax (name := grewriteSeq) "grewrite" optConfig rwRuleSeq (location)? : tactic -@[tactic grewriteSeq, inherit_doc grewriteSeq] def evalGRewriteSeq : Tactic := fun stx => do +@[tactic grewriteSeq, inherit_doc grewriteSeq] +public def evalGRewriteSeq : Tactic := fun stx => do let cfg ← elabGRewriteConfig stx[1] let loc := expandOptLocation stx[3] withRWRulesSeq stx[0] stx[2] fun symm term => do @@ -104,6 +127,19 @@ syntax (name := grewriteSeq) "grewrite" optConfig rwRuleSeq (location)? : tactic (grewriteTarget term symm cfg) (throwTacticEx `grewrite · "did not find instance of the pattern in the current goal") +@[tactic_alt grewriteSeq] +syntax (name := grewriteSeq') "grewrite'" optConfig rwRuleSeq (location)? : tactic + +@[tactic grewriteSeq', inherit_doc grewriteSeq] +public def evalGRewriteSeq' : Tactic := fun stx => do + let cfg ← elabGRewriteConfig stx[1] + let loc := expandOptLocation stx[3] + withRWRulesSeq stx[0] stx[2] fun symm term => do + withLocation loc + (grewriteLocalDecl' term symm · cfg) + (grewriteTarget' term symm cfg) + (throwTacticEx `grewrite · "did not find instance of the pattern in the current goal") + /-- `grw [e₁, ..., eₙ]` uses each expression `eᵢ : Rᵢ aᵢ bᵢ` (where `Rᵢ` is any two-argument relation) as a generalized rewrite rule on the main goal, replacing occurrences of `aᵢ` with `bᵢ`, @@ -164,6 +200,14 @@ macro (name := grwSeq) "grw " c:optConfig s:rwRuleSeq l:(location)? : tactic => `(tactic| (grewrite $c [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl)))) | _ => Macro.throwUnsupported +@[tactic_alt grwSeq] +macro (name := grwSeq') "grw' " c:optConfig s:rwRuleSeq l:(location)? : tactic => + match s with + | `(rwRuleSeq| [$rs,*]%$rbrak) => + -- We show the `rfl` state on `]` + `(tactic| (grewrite' $c [$rs,*] $(l)?; with_annotate_state $rbrak (try (with_reducible rfl)))) + | _ => Macro.throwUnsupported + /-- `apply_rewrite [e₁, ..., eₙ]` uses the expressions `e₁`, ..., `eₙ` as generalized rewrite rules, of type `pᵢ → qᵢ`, on the main goal, replacing occurrences of `pᵢ` with `qᵢ`. The difference with @@ -231,7 +275,7 @@ inequalities. * `nth_grewrite n₁ ... nₖ [e₁, ..., eₙ] at l` rewrites at the location(s) `l`. -/ macro "nth_grewrite" c:optConfig ppSpace nums:(num)+ s:rwRuleSeq loc:(location)? : tactic => do - `(tactic| grewrite $[$(getConfigItems c)]* (occs := .pos [$[$nums],*]) $s:rwRuleSeq $(loc)?) + `(tactic| grewrite' $[$(getConfigItems c)]* (occs := .pos [$[$nums],*]) $s:rwRuleSeq $(loc)?) /-- `nth_grw n₁ ... nₖ [e₁, ..., eₙ]` is a variant of `grw` that for each expression `eᵢ : R aᵢ bᵢ` only @@ -261,6 +305,6 @@ inequalities. * `nth_grw n₁ ... nₖ [e₁, ..., eₙ] at l` rewrites at the location(s) `l`. -/ macro "nth_grw" c:optConfig ppSpace nums:(num)+ s:rwRuleSeq loc:(location)? : tactic => do - `(tactic| grw $[$(getConfigItems c)]* (occs := .pos [$[$nums],*]) $s:rwRuleSeq $(loc)?) + `(tactic| grw' $[$(getConfigItems c)]* (occs := .pos [$[$nums],*]) $s:rwRuleSeq $(loc)?) -end Mathlib.Tactic +end Mathlib.Tactic.GRewrite diff --git a/Mathlib/Tactic/GRewrite/SinglePass.lean b/Mathlib/Tactic/GRewrite/SinglePass.lean new file mode 100644 index 00000000000000..f795702e55b037 --- /dev/null +++ b/Mathlib/Tactic/GRewrite/SinglePass.lean @@ -0,0 +1,258 @@ +/- +Copyright (c) 2026 Jovan Gerbscheid. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Jovan Gerbscheid +-/ +module + +public import Mathlib.Tactic.GRewrite.Core +public meta import Lean.Elab.Tactic.Rewrite + +/-! +# The generalized rewriting tactic 2.0 +-/ + +meta section + + +namespace Mathlib.Tactic.GRewrite + +open Lean Meta GCongr + +initialize registerTraceClass `Meta.grewrite +initialize registerTraceClass `Meta.grewrite.gcongr (inherited := true) + +structure GRewriteLemma where + symm : Bool + levelParams : Array Name := #[] + proof : Expr + numHyps? : Option Nat + headIdx : HeadIndex + headNumArgs : Nat + relName : Name + +abbrev GRewriteM := ReaderT GRewriteLemma + StateRefT (Std.HashSet (Option Expr × Expr × Bool)) GCongr.GCongrM + +def GRewriteLemma.getValue (lem : GRewriteLemma) : MetaM Expr := do + let us ← lem.levelParams.mapM fun _ => mkFreshLevelMVar + return lem.proof.instantiateLevelParamsArray lem.levelParams us + +def GRewriteLemma.metaTelescope (lem : GRewriteLemma) : MetaM (Array Expr × Expr × Expr) := do + let proof ← lem.getValue + let (mvars, _, rel) ← forallMetaTelescopeReducing (← inferType proof) lem.numHyps? + -- Use `Expr.beta` to get nicer looking proof terms. + return (mvars, rel, proof.beta mvars) + +def GRewriteLemma.apply (lem : GRewriteLemma) (g : MVarId) (symm : Bool) (config : Config) : + MetaM (Option (Array MVarId)) := do + withTraceNode `Meta.grewrite (fun _ ↦ return m!"applying grewrite lemma `{lem.proof}`") do + let (mvars, rel, proof) ← lem.metaTelescope + let (rel, proof) ← + if symm then + let proof ← try proof.applySymm catch _ => return none + pure (← inferType proof, proof) + else + pure (rel, proof) + let applied ← withConfig (fun oldConfig => { config, oldConfig with }) do + if ← isDefEq (← g.getType) rel then + g.assign proof; return true + else + let mctx ← getMCtx + for (n, tac) in (forwardExt.getState (← getEnv)).2 do + if n matches ``GCongr.exact | ``GCongr.symmExact | ``GCongr.exactRefl then continue + try tac.eval proof g; return true + catch _ => setMCtx mctx + return false + unless applied do return none + return some <| ← mvars.filterMapM fun mvar ↦ do + if ← mvar.mvarId!.isAssigned then return none + let type ← mvar.mvarId!.getType + if (← isClass? type).isSome then + if let .some inst ← trySynthInstance type then + mvar.mvarId!.assign inst + return none + return mvar.mvarId! + +def makeGCongrGoal (rel? : Option Expr) (e : Expr) (inv : Bool) : MetaM (Expr × Expr) := do + if let some rel := rel? then + -- Assume that `rel` is not heterogenous. + let mvar ← mkFreshExprMVar (← inferType e) + return (mvar, (if inv then mkApp2 rel mvar e else mkApp2 rel e mvar)) + else + let mvar ← mkFreshExprMVar (Expr.sort 0) + return (mvar, if inv then .forallE `_a mvar e .default else .forallE `_a e mvar .default) + +def getRel' (e : Expr) : Option (Name × Option Expr × Expr × Expr) := + match e with + | .app (.app rel lhs) rhs => rel.getAppFn.constName?.map (·, rel, lhs, rhs) + | .forallE _ lhs rhs _ => + if !rhs.hasLooseBVars then + some (`_Implies, none, lhs, rhs) + else + none + | _ => none + +mutual + +partial def processGCongrHypothesis (g : MVarId) (inv : Bool) (config : Config) : + GRewriteM Bool := g.withContext do + let some (relName, rel?, lhs, rhs) := getRel' (← whnf (← g.getType)) | + throwError "invalid `gcongr` goal {g}" + let (lhs, rhs) := if inv then (rhs, lhs) else (lhs, rhs) + if let some (result, proof) ← grewriteCore relName rel? lhs inv config then + rhs.withApp fun mvar xs ↦ do + mvar.mvarId!.assign (← mkLambdaFVars xs result) + g.assign proof + return true + else + return false + +partial def processGCongrLemma (g : MVarId) (lem : GCongrLemma) (inv : Bool) + (config : Config) : GRewriteM Bool := do + withTraceNode `Meta.grewrite.gcongr (fun _ ↦ return m!"applying {.ofConstName lem.declName}") do + let (mainGoals, sideGoals) ← try applyGCongrLemma g lem catch _ => return false + /- Firstly, synthesize instances to ensure that the lemma is applicable in this setting. + We allow synthesis to get stuck, because there are still metavariables to be filled in. -/ + let mut unsolvedSideGoals := #[] + for mvarId in sideGoals do + let type ← mvarId.getType + if (← isClass? type).isSome then + match ← trySynthInstance type with + | .some inst => mvarId.assign inst; continue + | .none => return false + | .undef => pure () + unsolvedSideGoals := unsolvedSideGoals.push mvarId + -- Then, recursively rewrite in the main subgoals + let mut anyProgress := false + for (g, isContra) in mainGoals do + if ← processGCongrHypothesis g (inv != isContra) config then + anyProgress := true + else + try g.applyRflOrId + catch _ => + trace[Meta.grewrite] "{← g.getType} could not be closed with `rfl`" + return false + -- Only continue if at least one rewrite happened + unless anyProgress do return false + -- Finally, close all remaining side goals + for mvarId in unsolvedSideGoals do + let type ← mvarId.getType + if (← isClass? type).isSome then + let some inst ← synthInstance? type | return false + mvarId.assign inst + else + dischargeSide mvarId + return true + +partial def grewriteCore (relName : Name) (rel? : Option Expr) (e : Expr) (inv : Bool) + (config : Config) : GRewriteM (Option (Expr × Expr)) := do + withTraceNodeBefore `Meta.grewrite (fun _ ↦ + return m!"visiting `{e}` with relation `{rel?.elim m!"→" (m!"{·}")}`") do + let e ← instantiateMVars e; let rel? ← rel?.mapM instantiateMVars + let cacheKey := (rel?, e, inv) + if (← get).contains cacheKey then + trace[Meta.grewrite] "cached: no rewrite" + return none + let (mvar, target) ← makeGCongrGoal rel? e inv + let g ← mkFreshExprMVar target + -- Try the given grewrite lemma. + let lem ← read + if e.toHeadIndex == lem.headIdx && e.headNumArgs == lem.headNumArgs then + if let some goals ← lem.apply g.mvarId! (inv != lem.symm) config then + goals.forM (pushNewGoal ·) + return (mvar, g) + -- Try all applicable `@[gcongr]` lemmas. + if let some (head, args) := getCongrAppFnArgs e then + let key := { relName, head, arity := args.size } + let lemmas := ((gcongrExt.getState (← getEnv)).get? key).getD (relImpRelLemma args.size) + let mctx ← getMCtx + for gcongrLem in lemmas do + if gcongrLem.forGrw then + if ← processGCongrLemma g.mvarId! gcongrLem inv config then + return (← instantiateMVars mvar, g) + setMCtx mctx + -- Cache the fact that there are no applicable lemmas + modify (·.insert cacheKey) + return none + +end + +def _root_.Lean.MVarId.grewrite (goal : MVarId) (e : Expr) (lem : GRewriteLemma) + (forwardImp : Bool) (config : Config) : MetaM GRewriteResult := + withReducible do goal.withContext do + goal.checkNotAssigned `grewrite + if let (some (eNew, impProof), newGoals) ← + grewriteCore `_Implies none e (!forwardImp) config |>.run lem |>.run' {} |>.run then + return { eNew, impProof, mvarIds := newGoals.toList } + else + let (_, rel, _) ← lem.metaTelescope + let some (_, lhs, rhs) := getRel (← whnf rel) | unreachable! + let pattern := if lem.symm then rhs else lhs + throwTacticEx `grewrite goal + m!"Did not find a suitable occurrence of {indentExpr pattern}\n\ + in the target expression{indentExpr e}" + +open Lean Meta Elab Parser + +def elabGRewriteLemma (stx : Syntax) (symm : Bool) (config : Config) : + TermElabM GRewriteLemma := do + Term.withoutModifyingElabMetaStateWithInfo do + -- Fully elaborate `stx`, not allowing e.g any postponed `by` blocks. + let e ← Term.elabTerm stx none + Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true) + let e ← instantiateMVars e + if e.hasSyntheticSorry then + throwAbortTactic + withReducible do + -- When using `apply_rw`, restrict the depth of the forall telescope. + let type ← inferType e + let numHyps? ← + if config.implicationHyp then + if let arity + 1 := type.getForallArity then + pure (some arity) + else + throwError m!"Invalid apply_rw argument: Expected an implication, not {type}" + else + pure none + let (mvars, _, rel) ← forallMetaTelescopeReducing (← inferType e) numHyps? + -- Since `a ≥ b` gets reduced to `b ≤ a`, we need to flip the rewrite direction. + let backward := rel.getAppFn'.constName?.any + (· matches ``GE.ge | ``GT.gt | ``Superset | ``SSuperset) + let symm := symm != backward + let some (relName, lhs, rhs) := getRel (← whnf rel) | + let valueDescr := if (← Meta.isProp rel) then "a proof of" else "a value of type" + throwError m!"Invalid grewrite argument: Expected a relation or definition name, \ + but{inlineExpr (e.beta mvars)}is {valueDescr}{indentExpr rel}" + -- Just like in `rw`, The head index and number of arguments determine where we try to rewrite. + let (headIdx, headNumArgs) := + if symm then (rhs.toHeadIndex, rhs.headNumArgs) else (lhs.toHeadIndex, lhs.headNumArgs) + if headIdx matches .mvar _ then + throwError "Invalid grewrite argument: The pattern to be substituted \ + is a metavariable (`{lhs}`) in this relation{indentExpr rel}" + let (levelParams, proof) ← + if e.hasMVar then + let r ← abstractMVars e + pure (r.paramNames, r.expr) + else + pure (#[], e) + return { symm, levelParams, proof, numHyps?, headIdx, headNumArgs, relName } + +public def elabGRewrite (mvarId : MVarId) (e : Expr) (stx : Syntax) (forwardImp symm : Bool) + (config : Config) : Tactic.TacticM GRewriteResult := do + let mvarCounterSaved := (← getMCtx).mvarCounter + let lem ← elabGRewriteLemma stx (symm := symm) (config := config) + if lem.relName matches ``Eq | ``Iff && config.useRewrite then + -- Elaborate `stx` again, so that we can use `Term.withSynthesize` + let { eNew, eqProof, mvarIds } ← Term.withSynthesize <| Tactic.elabRewrite mvarId e stx symm + let mp := if forwardImp then ``Eq.mp else ``Eq.mpr + let impProof ← mkAppOptM mp #[e, eNew, eqProof] + return { eNew, impProof, mvarIds } + let r ← mvarId.grewrite e lem forwardImp config + let mctx ← getMCtx + let mvarIds := r.mvarIds.filter fun mvarId => (mctx.getDecl mvarId |>.index) >= mvarCounterSaved + return { r with mvarIds } + +open Tactic + +end Mathlib.Tactic.GRewrite diff --git a/Mathlib/Topology/DiscreteSubset.lean b/Mathlib/Topology/DiscreteSubset.lean index 2d2d24190dedb3..f2f749aa43119d 100644 --- a/Mathlib/Topology/DiscreteSubset.lean +++ b/Mathlib/Topology/DiscreteSubset.lean @@ -132,7 +132,7 @@ lemma IsDiscrete.preimage' {s : Set Y} (hs : IsDiscrete s) (H : ∀ x, IsDiscrete (f ⁻¹' {x})) : IsDiscrete (f ⁻¹' s) := by refine .of_nhdsWithin fun x hx ↦ ?_ have h := ((H (f x)).nhdsWithin _ rfl).le - grw [nhdsWithin, ← comap_pure, ← hs.nhdsWithin _ hx, ← (hf.continuousWithinAt hx + grw' [nhdsWithin, ← comap_pure, ← hs.nhdsWithin _ hx, ← (hf.continuousWithinAt hx |>.tendsto_nhdsWithin fun _ ↦ by exact id).le_comap, inf_eq_right.mpr nhdsWithin_le_nhds] at h exact h diff --git a/Mathlib/Topology/EMetricSpace/Defs.lean b/Mathlib/Topology/EMetricSpace/Defs.lean index 2178faec407f83..ff66db567c8473 100644 --- a/Mathlib/Topology/EMetricSpace/Defs.lean +++ b/Mathlib/Topology/EMetricSpace/Defs.lean @@ -147,7 +147,7 @@ theorem edist_congr {w x y z : α} (hl : edist w x = 0) (hr : edist y z = 0) : (edist_congr_right hl).trans (edist_congr_left hr) theorem edist_triangle4 (x y z t : α) : edist x t ≤ edist x y + edist y z + edist z t := by - grw [edist_triangle _ z, edist_triangle] + grw [← edist_triangle, ← edist_triangle] /-- Reformulation of the uniform structure in terms of the extended distance -/ theorem uniformity_pseudoedist : 𝓤 α = ⨅ ε > 0, 𝓟 { p : α × α | edist p.1 p.2 < ε } := diff --git a/Mathlib/Topology/MetricSpace/Holder.lean b/Mathlib/Topology/MetricSpace/Holder.lean index 4a0b2b4c55e836..6e48e6a18ac91f 100644 --- a/Mathlib/Topology/MetricSpace/Holder.lean +++ b/Mathlib/Topology/MetricSpace/Holder.lean @@ -183,7 +183,7 @@ lemma holderOnWith_zero_of_bounded {C D : ℝ≥0} {A : Set X} HolderOnWith (C * D ^ (r : ℝ)) 0 f A := by intro x hx y hy simp only [NNReal.coe_zero, ENNReal.rpow_zero, mul_one] - grw [hf x hx y hy, hA x hx y hy, ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ (by simp)] + grw' [hf x hx y hy, hA x hx y hy, ENNReal.coe_mul, ENNReal.coe_rpow_of_nonneg _ (by simp)] /-- If a function is `r`-Hölder over a bounded set, then it is also `s`-Hölder when `s ≤ r`. -/ lemma of_le {C D s : ℝ≥0} {A : Set X} diff --git a/Mathlib/Topology/MetricSpace/ThickenedIndicator.lean b/Mathlib/Topology/MetricSpace/ThickenedIndicator.lean index 1e9ac9ed902486..16c8355c6f50db 100644 --- a/Mathlib/Topology/MetricSpace/ThickenedIndicator.lean +++ b/Mathlib/Topology/MetricSpace/ThickenedIndicator.lean @@ -228,6 +228,7 @@ theorem thickenedIndicator_subset {δ : ℝ} (δ_pos : 0 < δ) {E₁ E₂ : Set (toNNReal_le_toNNReal (by finiteness) (by finiteness)).mpr (thickenedIndicatorAux_subset δ subset x) +set_option linter.gcongr.grw false in @[gcongr] lemma thickenedIndicator_mono_infEDist {δ : ℝ} (δ_pos : 0 < δ) {E : Set α} {x y : α} (h : infEDist x E ≤ infEDist y E) : diff --git a/MathlibTest/GCongr/implications.lean b/MathlibTest/GCongr/implications.lean index 9f3c85f5639571..dea0aaf23c1d3e 100644 --- a/MathlibTest/GCongr/implications.lean +++ b/MathlibTest/GCongr/implications.lean @@ -25,3 +25,9 @@ example (h : c → b) : (a → b → c) → (a → b → b) := by example (h : ∀ n : Nat, 0 ≤ n) : ∀ n : Int, 0 ≤ n := by revert h gcongr + +-- Binder names are inferred, using the binder names in the LHS. +example (f g : Nat → Nat → Prop) (h : ∀ i j, f i j → g i j) : + (∃ ε > 0, ∃ δ > 0, f ε δ) → (∃ ε' > 0, ∃ δ' > 0, g ε' δ') := by + gcongr + exact h ε δ diff --git a/MathlibTest/GRewrite.lean b/MathlibTest/GRewrite.lean index 02d182d02c77eb..89fa2688bc8f07 100644 --- a/MathlibTest/GRewrite.lean +++ b/MathlibTest/GRewrite.lean @@ -50,8 +50,6 @@ example (h₁ : a + e ≤ b + e) (h₂ : b < c) (h₃ : c ≤ d) : a + e ≤ d + exact h₁ example (f g : α → α) (h : ∀ x : α, f x ≤ g x) (h₂ : g a + g b ≤ 5) : f a + f b ≤ 5 := by - grw [h] - guard_target =ₛ g a + f b ≤ 5 grw [h] guard_target =ₛ g a + g b ≤ 5 grw [h₂] @@ -89,7 +87,8 @@ However, the current behavior is easier to implement, and preserves the form of which is a useful invariant. -/ example {x y z : ℤ} (hx : x < y) : 2 * x < z := by grw [hx] - guard_target =ₛ 2 * y < z + fail_if_success guard_target =ₛ 2 * y < z + guard_target = 2 * y < z exact test_sorry end inequalities @@ -135,7 +134,7 @@ example {x y z : ℚ} (f g : ℚ → ℚ) (h : ∀ t, f t = g t) : 2 * f x * f y example {x y a b : ℚ} (h : x ≤ y) (h1 : a ≤ 3 * x) : 2 * x ≤ b := by grw [h] at h1 - guard_hyp h1 :ₛ a ≤ 3 * y + guard_hyp h1 : a ≤ 3 * y exact test_sorry end rationals @@ -185,8 +184,8 @@ example {a b : ℤ} (h1 : a ≡ 3 [ZMOD 5]) (h2 : b ≡ a ^ 2 + 1 [ZMOD 5]) : example {x y a b : ℚ} (h : x < y) (h1 : a ≤ 3 * x) : 2 * x ≤ b := by grw [h] at * guard_hyp h :ₛ x < y -- `grw [h] at *` does not rewrite at `h` - guard_hyp h1 :ₛ a ≤ 3 * y - guard_target =ₛ 2 * y ≤ b + guard_hyp h1 : a ≤ 3 * y + guard_target = 2 * y ≤ b exact test_sorry end wildcard @@ -213,12 +212,14 @@ relation does not have its main goals proved by `gcongr` (in the two examples he the inequality goes in the wrong direction). -/ /-- -error: Tactic `grewrite` failed: could not discharge x ≤ y using x ≥ y +error: Tactic `grewrite` failed: Did not find a suitable occurrence of ⏎ + x +in the target expression + 2 * x ≤ b -case h₁.hbc x y b : ℚ h : x ≥ y -⊢ x ≤ y +⊢ 2 * x ≤ b -/ #guard_msgs in example {x y b : ℚ} (h : x ≥ y) : 2 * x ≤ b := by @@ -254,18 +255,9 @@ example {Prime : ℕ → Prop} {a a' : ℕ} (h₁ : Prime (a + 1)) (h₂ : a = a guard_hyp h₁ :ₛ Prime (a' + 1) exact test_sorry -/-- -error: Tactic `grewrite` failed: could not discharge b ≤ a using a ≤ b - -case h₂.hbc -a b c : ℚ -h₁ : a ≤ b -h₂ : 0 ≤ c -⊢ b ≤ a --/ -#guard_msgs in example {a b c : ℚ} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≥ 100 + a := by grw [h₁] + exact test_sorry example {a b c : ℚ} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≥ 100 + a + a := by nth_grw 2 3 [h₁] @@ -300,7 +292,7 @@ end apply -- previously, `grw` failed to rewrite in expressions with syntheticOpaque metavariables example : ∃ n, n < 2 := by refine ⟨?_, ?_⟩ - on_goal 2 => grw [← one_lt_two] + on_goal 2 => grw [← one_le_two] exact 0 refine zero_lt_one @@ -360,8 +352,10 @@ example (h : double (double 2) ≤ 10) : double 4 ≤ 20 := by -- `rw`/`grw` index based on the head constant, so the following fails. /-- -error: Tactic `grewrite` failed: did not find instance of the pattern in the target expression +error: Tactic `grewrite` failed: Did not find a suitable occurrence of ⏎ double 2 +in the target expression + 4 ≤ 20 h : double 2 ≤ 10 ⊢ 4 ≤ 20 @@ -371,3 +365,11 @@ example (h : double 2 ≤ 10) : 4 ≤ 20 := by grw (transparency := default) [h] end erw + +section binders + +lemma biSup_inf_le {α β : Type*} [CompleteLattice β] (f : α → β) (s : Set α) (b : β) : + ⨆ a ∈ s, (f a ⊓ b) ≤ (⨆ a ∈ s, f a) ⊓ b := by + grw [iSup_inf_le_iSup_inf, iSup_inf_le_iSup_inf] + +end binders