diff --git a/Archive/Imo/Imo2024Q5.lean b/Archive/Imo/Imo2024Q5.lean index 4fa8394b08d3d6..04b40fc9ee4e20 100644 --- a/Archive/Imo/Imo2024Q5.lean +++ b/Archive/Imo/Imo2024Q5.lean @@ -302,7 +302,7 @@ lemma Path.tail_induction {motive : Path N → Prop} (ind : ∀ p, motive p.tail case cons head tail hi => by_cases h : (p'.cells[1]'p'.one_lt_length_cells).1 = 0 · refine ind p' ?_ - simp_rw [Path.tail, if_pos h, List.tail_cons] + simp_rw [Path.tail, if_pos h, p', List.tail_cons] exact hi _ _ _ _ · exact base p' h diff --git a/Mathlib.lean b/Mathlib.lean index 3a6ceab1f6a98b..f692eadfdec90f 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -4841,7 +4841,6 @@ import Mathlib.Tactic.DefEqTransformations import Mathlib.Tactic.DeprecateTo import Mathlib.Tactic.DeriveCountable import Mathlib.Tactic.DeriveFintype -import Mathlib.Tactic.DeriveToExpr import Mathlib.Tactic.DeriveTraversable import Mathlib.Tactic.Eqns import Mathlib.Tactic.Eval diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean index f336a553c7f571..045c79a9465a3d 100644 --- a/Mathlib/Algebra/BigOperators/Fin.lean +++ b/Mathlib/Algebra/BigOperators/Fin.lean @@ -162,7 +162,7 @@ theorem prod_Ioi_succ {M : Type*} [CommMonoid M] {n : ℕ} (i : Fin n) (v : Fin @[to_additive] theorem prod_congr' {M : Type*} [CommMonoid M] {a b : ℕ} (f : Fin b → M) (h : a = b) : - (∏ i : Fin a, f (cast h i)) = ∏ i : Fin b, f i := by + (∏ i : Fin a, f (i.cast h)) = ∏ i : Fin b, f i := by subst h congr diff --git a/Mathlib/Algebra/BigOperators/Group/List.lean b/Mathlib/Algebra/BigOperators/Group/List.lean index 1dd09cee528535..5ff4cb25da33e0 100644 --- a/Mathlib/Algebra/BigOperators/Group/List.lean +++ b/Mathlib/Algebra/BigOperators/Group/List.lean @@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Floris van Doorn, Sébastien Gouëzel, Alex J. Best -/ import Mathlib.Algebra.Divisibility.Basic import Mathlib.Algebra.Group.Int -import Mathlib.Data.List.Lemmas import Mathlib.Data.List.Dedup import Mathlib.Data.List.Flatten import Mathlib.Data.List.Pairwise @@ -637,10 +636,6 @@ end MonoidHom end MonoidHom -set_option linter.deprecated false in -@[simp, deprecated "No deprecation message was provided." (since := "2024-10-17")] -lemma Nat.sum_eq_listSum (l : List ℕ) : Nat.sum l = l.sum := rfl - namespace List lemma length_sigma {σ : α → Type*} (l₁ : List α) (l₂ : ∀ a, List (σ a)) : diff --git a/Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean b/Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean index 9b5e8cdc2e08b7..05caccfa0a1a74 100644 --- a/Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean +++ b/Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean @@ -146,7 +146,7 @@ lemma schwartz_zippel_sup_sum : calc #{x₀ ∈ S 0 | eval (cons x₀ xₜ) p = 0} ≤ #pₓ.roots.toFinset := by gcongr - simp (config := { contextual := true }) [subset_iff, eval_eq_eval_mv_eval', pₓ, hpₓ₀] + simp +contextual [subset_iff, eval_eq_eval_mv_eval', pₓ, hpₓ₀, p'] _ ≤ Multiset.card pₓ.roots := pₓ.roots.toFinset_card_le _ ≤ pₓ.natDegree := pₓ.card_roots' _ = k := hpₓdeg diff --git a/Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean b/Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean index 5738f216555e7d..0bce274b8d0381 100644 --- a/Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean +++ b/Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean @@ -425,7 +425,8 @@ theorem toCharThreeNF_spec_of_b₂_ne_zero (hb₂ : W.b₂ ≠ 0) : constructor · simp · simp - · field_simp [W.toShortNFOfCharThree_a₂ ▸ hb₂] + · have ha₂ : W'.a₂ ≠ 0 := W.toShortNFOfCharThree_a₂ ▸ hb₂ + field_simp [ha₂] linear_combination (W'.a₄ * W'.a₂ ^ 2 + W'.a₄ ^ 2) * CharP.cast_eq_zero F 3 theorem toCharThreeNF_spec_of_b₂_eq_zero (hb₂ : W.b₂ = 0) : diff --git a/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean b/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean index 347525ce0df814..0ebab41ba1c2aa 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean @@ -401,10 +401,10 @@ def extendMiddle (c : OrderedFinpartition n) (k : Fin c.length) : OrderedFinpart rcases eq_or_ne (c.index i) k with rfl | hi · have A : update c.partSize (c.index i) (c.partSize (c.index i) + 1) (c.index i) = c.partSize (c.index i) + 1 := by simp - exact ⟨c.index i, cast A.symm (succ (c.invEmbedding i)), by simp⟩ + exact ⟨c.index i, (succ (c.invEmbedding i)).cast A.symm , by simp⟩ · have A : update c.partSize k (c.partSize k + 1) (c.index i) = c.partSize (c.index i) := by simp [hi] - exact ⟨c.index i, cast A.symm (c.invEmbedding i), by simp [hi]⟩ + exact ⟨c.index i, (c.invEmbedding i).cast A.symm, by simp [hi]⟩ lemma index_extendMiddle_zero (c : OrderedFinpartition n) (i : Fin c.length) : (c.extendMiddle i).index 0 = i := by @@ -678,8 +678,8 @@ def extendEquiv (n : ℕ) : · simp only [↓reduceDIte, comp_apply] rcases eq_or_ne j 0 with rfl | hj · simpa using c.emb_zero - · let j' := Fin.pred (cast B.symm j) (by simpa using hj) - have : j = cast B (succ j') := by simp [j'] + · let j' := Fin.pred (j.cast B.symm) (by simpa using hj) + have : j = (succ j').cast B := by simp [j'] simp only [this, coe_cast, val_succ, cast_mk, cases_succ', comp_apply, succ_mk, Nat.succ_eq_add_one, succ_pred] rfl diff --git a/Mathlib/Analysis/Convex/Continuous.lean b/Mathlib/Analysis/Convex/Continuous.lean index fc4bc36368d8b3..608b5a05cc364d 100644 --- a/Mathlib/Analysis/Convex/Continuous.lean +++ b/Mathlib/Analysis/Convex/Continuous.lean @@ -51,7 +51,8 @@ lemma ConvexOn.lipschitzOnWith_of_abs_le (hf : ConvexOn ℝ (ball x₀ r) f) (h ε * (f x - f y) ≤ ‖x - y‖ * (f z - f x) := by rw [mul_sub, mul_sub, sub_le_sub_iff, ← add_mul] have h := hf.2 hy' hz (by positivity) (by positivity) hab - field_simp [← hxyz, a, b, ← mul_div_right_comm] at h + rw [← hxyz] at h + field_simp [a, b, ← mul_div_right_comm] at h rwa [← le_div_iff₀' (by positivity), add_comm (_ * _)] _ ≤ _ := by rw [sub_eq_add_neg (f _), two_mul] diff --git a/Mathlib/CategoryTheory/Galois/Decomposition.lean b/Mathlib/CategoryTheory/Galois/Decomposition.lean index 7b77438602714d..0266fabf8bc160 100644 --- a/Mathlib/CategoryTheory/Galois/Decomposition.lean +++ b/Mathlib/CategoryTheory/Galois/Decomposition.lean @@ -154,12 +154,14 @@ lemma connected_component_unique {X A B : C} [IsConnected A] [IsConnected B] (a have : IsIso v := IsConnected.noTrivialComponent Y v hn use (asIso u).symm ≪≫ asIso v have hu : G.map u y = a := by - simp only [y, e, ← PreservesPullback.iso_hom_fst G, fiberPullbackEquiv, Iso.toEquiv_comp, - Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply, inv_hom_id_apply] + simp only [u, G, y, e, ← PreservesPullback.iso_hom_fst G, fiberPullbackEquiv, + Iso.toEquiv_comp, Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply, + inv_hom_id_apply] erw [Types.pullbackIsoPullback_inv_fst_apply (F.map i) (F.map j)] have hv : G.map v y = b := by - simp only [y, e, ← PreservesPullback.iso_hom_snd G, fiberPullbackEquiv, Iso.toEquiv_comp, - Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply, inv_hom_id_apply] + simp only [v, G, y, e, ← PreservesPullback.iso_hom_snd G, fiberPullbackEquiv, + Iso.toEquiv_comp, Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply, + inv_hom_id_apply] erw [Types.pullbackIsoPullback_inv_snd_apply (F.map i) (F.map j)] rw [← hu, ← hv] show (F.toPrefunctor.map u ≫ F.toPrefunctor.map _) y = F.toPrefunctor.map v y diff --git a/Mathlib/Computability/TMToPartrec.lean b/Mathlib/Computability/TMToPartrec.lean index 232291b05955f7..e0c093182ad2c1 100644 --- a/Mathlib/Computability/TMToPartrec.lean +++ b/Mathlib/Computability/TMToPartrec.lean @@ -1238,7 +1238,7 @@ theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁ swap · rw [Function.update_of_ne h₁.symm, List.reverseAux_nil] refine TransGen.head' rfl ?_ - simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim, ne_eq] + rw [tr]; simp only [pop', TM2.stepAux] revert e; cases' S k₁ with a Sk <;> intro e · cases e rfl @@ -1248,7 +1248,7 @@ theorem move_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k₁ simp only [e] rfl · refine TransGen.head rfl ?_ - simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim, ne_eq, List.reverseAux_cons] + rw [tr]; simp only [pop', Option.elim, TM2.stepAux, push'] cases' e₁ : S k₁ with a' Sk <;> rw [e₁, splitAtPred] at e · cases e cases e₂ : p a' <;> simp only [e₂, cond] at e @@ -1273,16 +1273,15 @@ theorem move₂_ok {p k₁ k₂ q s L₁ o L₂} {S : K' → List Γ'} (h₁ : k ⟨some q, none, update (update S k₁ (o.elim id List.cons L₂)) k₂ (L₁ ++ S k₂)⟩ := by refine (move_ok h₁.1 e).trans (TransGen.head rfl ?_) simp only [TM2.step, Option.mem_def, TM2.stepAux, id_eq, ne_eq, Option.elim] - cases o <;> simp only [Option.elim, id] - · simp only [TM2.stepAux, Option.isSome, cond_false] - convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2 + cases o <;> simp only [Option.elim] <;> rw [tr] + <;> simp only [id, TM2.stepAux, Option.isSome, cond_true, cond_false] + · convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2 simp only [Function.update_comm h₁.1, Function.update_idem] rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]] simp only [Function.update_of_ne h₁.2.2.symm, Function.update_of_ne h₁.2.1, Function.update_of_ne h₁.1.symm, List.reverseAux_eq, h₂, Function.update_self, List.append_nil, List.reverse_reverse] - · simp only [TM2.stepAux, Option.isSome, cond_true] - convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2 + · convert move_ok h₁.2.1.symm (splitAtPred_false _) using 2 simp only [h₂, Function.update_comm h₁.1, List.reverseAux_eq, Function.update_self, List.append_nil, Function.update_idem] rw [show update S rev [] = S by rw [← h₂, Function.update_eq_self]] @@ -1293,7 +1292,7 @@ theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p Reaches₁ (TM2.step tr) ⟨some (Λ'.clear p k q), s, S⟩ ⟨some q, o, update S k L₂⟩ := by induction' L₁ with a L₁ IH generalizing S s · refine TransGen.head' rfl ?_ - simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim] + rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim] revert e; cases' S k with a Sk <;> intro e · cases e rfl @@ -1303,7 +1302,7 @@ theorem clear_ok {p k q s L₁ o L₂} {S : K' → List Γ'} (e : splitAtPred p rcases e with ⟨e₁, e₂⟩ rw [e₁, e₂] · refine TransGen.head rfl ?_ - simp only [TM2.step, Option.mem_def, TM2.stepAux, Option.elim] + rw [tr]; simp only [pop', TM2.step, Option.mem_def, TM2.stepAux, Option.elim] cases' e₁ : S k with a' Sk <;> rw [e₁, splitAtPred] at e · cases e cases e₂ : p a' <;> simp only [e₂, cond] at e @@ -1322,9 +1321,10 @@ theorem copy_ok (q s a b c d) : · refine TransGen.single ?_ simp refine TransGen.head rfl ?_ + rw [tr] simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_rev, List.head?_cons, Option.isSome_some, List.tail_cons, elim_update_rev, ne_eq, Function.update_of_ne, elim_main, elim_update_main, - elim_stack, elim_update_stack, cond_true, List.reverseAux_cons] + elim_stack, elim_update_stack, cond_true, List.reverseAux_cons, pop', push'] exact IH _ _ _ theorem trPosNum_natEnd : ∀ (n), ∀ x ∈ trPosNum n, natEnd x = false @@ -1358,6 +1358,7 @@ theorem head_main_ok {q s L} {c d : List Γ'} : (splitAtPred_eq _ _ (trNat L.headI) o (trList L.tail) (trNat_natEnd _) ?_)).trans (TransGen.head rfl (TransGen.head rfl ?_)) · cases L <;> simp [o] + rw [tr] simp only [TM2.step, Option.mem_def, TM2.stepAux, elim_update_main, elim_rev, elim_update_rev, Function.update_self, trList] rw [if_neg (show o ≠ some Γ'.consₗ by cases L <;> simp [o])] @@ -1375,6 +1376,7 @@ theorem head_stack_ok {q s L₁ L₂ L₃} : (move_ok (by decide) (splitAtPred_eq _ _ [] (some Γ'.consₗ) L₃ (by rintro _ ⟨⟩) ⟨rfl, rfl⟩)) (TransGen.head rfl (TransGen.head rfl ?_)) + rw [tr] simp only [TM2.step, Option.mem_def, TM2.stepAux, ite_true, id_eq, trList, List.nil_append, elim_update_stack, elim_rev, List.reverseAux_nil, elim_update_rev, Function.update_self, List.headI_nil, trNat_default] @@ -1428,7 +1430,8 @@ theorem succ_ok {q s n} {c d : List Γ'} : simp [PosNum.succ, trPosNum] rfl · refine ⟨l₁, _, some Γ'.bit0, rfl, TransGen.single ?_⟩ - simp only [TM2.step, TM2.stepAux, elim_main, elim_update_main, ne_eq, Function.update_of_ne, + simp only [TM2.step]; rw [tr] + simp only [TM2.stepAux, pop', elim_main, elim_update_main, ne_eq, Function.update_of_ne, elim_rev, elim_update_rev, Function.update_self, Option.mem_def, Option.some.injEq] rfl @@ -1445,11 +1448,9 @@ theorem pred_ok (q₁ q₂ s v) (c d : List Γ') : ∃ s', simp only [TM2.step, trList, trNat.eq_1, trNum, Nat.cast_succ, Num.add_one, Num.succ, List.tail_cons, List.headI_cons] cases' (n : Num) with a - · simp only [trPosNum, List.singleton_append, List.nil_append] + · simp only [trPosNum, Num.succ', List.singleton_append, List.nil_append] refine TransGen.head rfl ?_ - simp only [Option.mem_def, TM2.stepAux, elim_main, List.head?_cons, Option.some.injEq, - decide_false, List.tail_cons, elim_update_main, ne_eq, Function.update_of_ne, elim_rev, - elim_update_rev, natEnd, Function.update_self, cond_true, cond_false] + rw [tr]; simp only [pop', TM2.stepAux, cond_false] convert unrev_ok using 2 simp simp only [Num.succ'] @@ -1555,13 +1556,11 @@ theorem tr_ret_respects (k v s) : ∃ b₂, by_cases h : v.headI = 0 <;> simp only [h, ite_true, ite_false] at this ⊢ · obtain ⟨c, h₁, h₂⟩ := IH v.tail (trList v).head? refine ⟨c, h₁, TransGen.head rfl ?_⟩ - simp only [Option.mem_def, TM2.stepAux, trContStack, contStack, elim_main, this, cond_true, - elim_update_main] + rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this, elim_update_main] exact h₂ · obtain ⟨s', h₁, h₂⟩ := trNormal_respects f (Cont.fix f k) v.tail (some Γ'.cons) refine ⟨_, h₁, TransGen.head rfl <| TransGen.trans ?_ h₂⟩ - simp only [Option.mem_def, TM2.stepAux, elim_main, this.1, cond_false, elim_update_main, - trCont] + rw [trCont, tr]; simp only [pop', TM2.stepAux, elim_main, this.1] convert clear_ok (splitAtPred_eq _ _ (trNat v.headI).tail (some Γ'.cons) _ _ _) using 2 · simp convert rfl diff --git a/Mathlib/Computability/TuringMachine.lean b/Mathlib/Computability/TuringMachine.lean index 919e0be38ca9fd..2d124e2707b94d 100644 --- a/Mathlib/Computability/TuringMachine.lean +++ b/Mathlib/Computability/TuringMachine.lean @@ -1828,12 +1828,12 @@ theorem tr_respects : Respects (TM0.step M) (TM1.step (tr M)) fun a b ↦ trCfg cases' s with d a <;> rfl intro e refine TransGen.head ?_ (TransGen.head' this ?_) - · simp only [TM1.step, TM1.stepAux] + · simp only [TM1.step, TM1.stepAux, tr] rw [e] rfl cases e' : M q' _ · apply ReflTransGen.single - simp only [TM1.step, TM1.stepAux] + simp only [TM1.step, TM1.stepAux, tr] rw [e'] rfl · rfl @@ -1926,7 +1926,6 @@ section variable [DecidableEq K] /-- The step function for the TM2 model. -/ -@[simp] def stepAux : Stmt₂ → σ → (∀ k, List (Γ k)) → Cfg₂ | push k f q, v, S => stepAux q v (update S k (f v :: S k)) | peek k f q, v, S => stepAux q (f v (S k).head?) S @@ -1937,11 +1936,13 @@ def stepAux : Stmt₂ → σ → (∀ k, List (Γ k)) → Cfg₂ | halt, v, S => ⟨none, v, S⟩ /-- The step function for the TM2 model. -/ -@[simp] def step (M : Λ → Stmt₂) : Cfg₂ → Option Cfg₂ | ⟨none, _, _⟩ => none | ⟨some l, v, S⟩ => some (stepAux (M l) v S) +attribute [simp] stepAux.eq_1 stepAux.eq_2 stepAux.eq_3 + stepAux.eq_4 stepAux.eq_5 stepAux.eq_6 stepAux.eq_7 step.eq_1 step.eq_2 + /-- The (reflexive) reachability relation for the TM2 model. -/ def Reaches (M : Λ → Stmt₂) : Cfg₂ → Cfg₂ → Prop := ReflTransGen fun a b ↦ b ∈ step M a @@ -2292,7 +2293,7 @@ noncomputable def trStmts₁ : Stmt₂ → Finset Λ'₂₁ theorem trStmts₁_run {k : K} {s : StAct₂ k} {q : Stmt₂} : trStmts₁ (stRun s q) = {go k s q, ret q} ∪ trStmts₁ q := by - cases s <;> simp only [trStmts₁] + cases s <;> simp only [trStmts₁, stRun] theorem tr_respects_aux₂ [DecidableEq K] {k : K} {q : Stmt₂₁} {v : σ} {S : ∀ k, List (Γ k)} {L : ListBlank (∀ k, Option (Γ k))} diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 11123477cd16a4..6056e283f70cc8 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -269,7 +269,7 @@ This one instead uses a `NeZero n` typeclass hypothesis. theorem pos_iff_ne_zero' [NeZero n] (a : Fin n) : 0 < a ↔ a ≠ 0 := by rw [← val_fin_lt, val_zero', Nat.pos_iff_ne_zero, Ne, Ne, Fin.ext_iff, val_zero'] -@[simp] lemma cast_eq_self (a : Fin n) : cast rfl a = a := rfl +@[simp] lemma cast_eq_self (a : Fin n) : a.cast rfl = a := rfl @[simp] theorem cast_eq_zero {k l : ℕ} [NeZero k] [NeZero l] (h : k = l) (x : Fin k) : Fin.cast h x = 0 ↔ x = 0 := by simp [← val_eq_val] @@ -299,7 +299,7 @@ theorem revPerm_symm : (@revPerm n).symm = revPerm := rfl theorem cast_rev (i : Fin n) (h : n = m) : - cast h i.rev = (i.cast h).rev := by + i.rev.cast h = (i.cast h).rev := by subst h; simp theorem rev_eq_iff {i j : Fin n} : rev i = j ↔ i = rev j := by @@ -619,23 +619,23 @@ theorem coe_of_injective_castLE_symm {n k : ℕ} (h : n ≤ k) (i : Fin k) (hi) rw [← coe_castLE h] exact congr_arg Fin.val (Equiv.apply_ofInjective_symm _ _) -theorem leftInverse_cast (eq : n = m) : LeftInverse (cast eq.symm) (cast eq) := +theorem leftInverse_cast (eq : n = m) : LeftInverse (Fin.cast eq.symm) (Fin.cast eq) := fun _ => rfl -theorem rightInverse_cast (eq : n = m) : RightInverse (cast eq.symm) (cast eq) := +theorem rightInverse_cast (eq : n = m) : RightInverse (Fin.cast eq.symm) (Fin.cast eq) := fun _ => rfl -theorem cast_lt_cast (eq : n = m) {a b : Fin n} : cast eq a < cast eq b ↔ a < b := +theorem cast_lt_cast (eq : n = m) {a b : Fin n} : a.cast eq < b.cast eq ↔ a < b := Iff.rfl -theorem cast_le_cast (eq : n = m) {a b : Fin n} : cast eq a ≤ cast eq b ↔ a ≤ b := +theorem cast_le_cast (eq : n = m) {a b : Fin n} : a.cast eq ≤ b.cast eq ↔ a ≤ b := Iff.rfl /-- The 'identity' equivalence between `Fin m` and `Fin n` when `m = n`. -/ @[simps] def _root_.finCongr (eq : n = m) : Fin n ≃ Fin m where - toFun := cast eq - invFun := cast eq.symm + toFun := Fin.cast eq + invFun := Fin.cast eq.symm left_inv := leftInverse_cast eq right_inv := rightInverse_cast eq @@ -656,12 +656,12 @@ a generic theorem about `cast`. -/ lemma _root_.finCongr_eq_equivCast (h : n = m) : finCongr h = .cast (h ▸ rfl) := by subst h; simp @[simp] -theorem cast_zero {n' : ℕ} [NeZero n] {h : n = n'} : cast h (0 : Fin n) = +theorem cast_zero {n' : ℕ} [NeZero n] {h : n = n'} : (0 : Fin n).cast h = by { haveI : NeZero n' := by {rw [← h]; infer_instance}; exact 0} := rfl /-- While in many cases `Fin.cast` is better than `Equiv.cast`/`cast`, sometimes we want to apply a generic theorem about `cast`. -/ -theorem cast_eq_cast (h : n = m) : (cast h : Fin n → Fin m) = _root_.cast (h ▸ rfl) := by +theorem cast_eq_cast (h : n = m) : (Fin.cast h : Fin n → Fin m) = _root_.cast (h ▸ rfl) := by subst h ext rfl diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean index 72ddaaa0b028e1..3a31ba890f95d6 100644 --- a/Mathlib/Data/Fin/Tuple/Basic.lean +++ b/Mathlib/Data/Fin/Tuple/Basic.lean @@ -395,7 +395,7 @@ theorem cons_eq_append (x : α) (xs : Fin n → α) : subst h; simp lemma append_rev {m n} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)) : - append xs ys (rev i) = append (ys ∘ rev) (xs ∘ rev) (cast (Nat.add_comm ..) i) := by + append xs ys (rev i) = append (ys ∘ rev) (xs ∘ rev) (i.cast (Nat.add_comm ..)) := by rcases rev_surjective i with ⟨i, rfl⟩ rw [rev_rev] induction i using Fin.addCases @@ -403,7 +403,7 @@ lemma append_rev {m n} (xs : Fin m → α) (ys : Fin n → α) (i : Fin (m + n)) · simp [cast_rev, rev_addNat] lemma append_comp_rev {m n} (xs : Fin m → α) (ys : Fin n → α) : - append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ cast (Nat.add_comm ..) := + append xs ys ∘ rev = append (ys ∘ rev) (xs ∘ rev) ∘ Fin.cast (Nat.add_comm ..) := funext <| append_rev xs ys theorem append_castAdd_natAdd {f : Fin (m + n) → α} : @@ -430,11 +430,11 @@ theorem repeat_apply (a : Fin n → α) (i : Fin (m * n)) : @[simp] theorem repeat_zero (a : Fin n → α) : - Fin.repeat 0 a = Fin.elim0 ∘ cast (Nat.zero_mul _) := - funext fun x => (cast (Nat.zero_mul _) x).elim0 + Fin.repeat 0 a = Fin.elim0 ∘ Fin.cast (Nat.zero_mul _) := + funext fun x => (x.cast (Nat.zero_mul _)).elim0 @[simp] -theorem repeat_one (a : Fin n → α) : Fin.repeat 1 a = a ∘ cast (Nat.one_mul _) := by +theorem repeat_one (a : Fin n → α) : Fin.repeat 1 a = a ∘ Fin.cast (Nat.one_mul _) := by generalize_proofs h apply funext rw [(Fin.rightInverse_cast h.symm).surjective.forall] @@ -443,7 +443,7 @@ theorem repeat_one (a : Fin n → α) : Fin.repeat 1 a = a ∘ cast (Nat.one_mul theorem repeat_succ (a : Fin n → α) (m : ℕ) : Fin.repeat m.succ a = - append a (Fin.repeat m a) ∘ cast ((Nat.succ_mul _ _).trans (Nat.add_comm ..)) := by + append a (Fin.repeat m a) ∘ Fin.cast ((Nat.succ_mul _ _).trans (Nat.add_comm ..)) := by generalize_proofs h apply funext rw [(Fin.rightInverse_cast h.symm).surjective.forall] @@ -453,7 +453,7 @@ theorem repeat_succ (a : Fin n → α) (m : ℕ) : @[simp] theorem repeat_add (a : Fin n → α) (m₁ m₂ : ℕ) : Fin.repeat (m₁ + m₂) a = - append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ cast (Nat.add_mul ..) := by + append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ Fin.cast (Nat.add_mul ..) := by generalize_proofs h apply funext rw [(Fin.rightInverse_cast h.symm).surjective.forall] diff --git a/Mathlib/Data/Fin/Tuple/Take.lean b/Mathlib/Data/Fin/Tuple/Take.lean index 232622468b1535..56346dbf9bff52 100644 --- a/Mathlib/Data/Fin/Tuple/Take.lean +++ b/Mathlib/Data/Fin/Tuple/Take.lean @@ -132,7 +132,7 @@ theorem take_addCases_right {n' : ℕ} {motive : Fin (n + n') → Sort*} (m : by_cases h' : i < n · simp only [h', ↓reduceDIte] congr - · simp only [h', ↓reduceDIte, subNat, castLE, cast, eqRec_eq_cast] + · simp only [h', ↓reduceDIte, subNat, castLE, Fin.cast, eqRec_eq_cast] /-- Version of `take_addCases_right` that specializes `addCases` to `append`. -/ theorem take_append_right {n' : ℕ} {α : Sort*} (m : ℕ) (h : m ≤ n') (u : (i : Fin n) → α) diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index e7ab67fafc45c4..3e4f9127bad670 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -399,8 +399,6 @@ theorem shiftRight_add' : ∀ (m : ℤ) (n k : ℕ), m >>> (n + k : ℤ) = (m >> /-! ### bitwise ops -/ -attribute [local simp] Int.zero_div - theorem shiftLeft_add : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (n + k) = (m <<< (n : ℤ)) <<< k | (m : ℕ), n, (k : ℕ) => congr_arg ofNat (by simp [Nat.shiftLeft_eq, Nat.pow_add, mul_assoc]) diff --git a/Mathlib/Data/Int/Lemmas.lean b/Mathlib/Data/Int/Lemmas.lean index f98d34103dd0d7..c51bbeb9c0106b 100644 --- a/Mathlib/Data/Int/Lemmas.lean +++ b/Mathlib/Data/Int/Lemmas.lean @@ -112,9 +112,6 @@ theorem toNat_of_nonpos : ∀ {z : ℤ}, z ≤ 0 → z.toNat = 0 This lemma is orphaned from `Data.Int.Bitwise` as it also requires material from `Data.Int.Order`. -/ - -attribute [local simp] Int.zero_div - @[simp] theorem div2_bit (b n) : div2 (bit b n) = n := by rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add] diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index dfd2fc1bb362c0..4c99fc84425e54 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -211,9 +211,6 @@ theorem eq_replicate_length {a : α} : ∀ {l : List α}, l = replicate l.length theorem replicate_add (m n) (a : α) : replicate (m + n) a = replicate m a ++ replicate n a := by rw [append_replicate_replicate] -theorem replicate_succ' (n) (a : α) : replicate (n + 1) a = replicate n a ++ [a] := - replicate_add n 1 a - theorem replicate_subset_singleton (n) (a : α) : replicate n a ⊆ [a] := fun _ h => mem_singleton.2 (eq_of_mem_replicate h) @@ -300,7 +297,7 @@ theorem getLast_append' (l₁ l₂ : List α) (h : l₂ ≠ []) : | nil => simp | cons _ _ ih => simp only [cons_append]; rw [List.getLast_cons]; exact ih -theorem getLast_concat' {a : α} (l : List α) : getLast (concat l a) (concat_ne_nil a l) = a := by +theorem getLast_concat' {a : α} (l : List α) : getLast (concat l a) (by simp) = a := by simp @[simp] @@ -487,10 +484,6 @@ theorem forall_mem_iff_getElem {l : List α} {p : α → Prop} : (∀ x ∈ l, p x) ↔ ∀ (i : ℕ) (_ : i < l.length), p l[i] := by simp [mem_iff_getElem, @forall_swap α] -theorem getElem_cons {l : List α} {a : α} {n : ℕ} (h : n < (a :: l).length) : - (a :: l)[n] = if hn : n = 0 then a else l[n - 1]'(by rw [length_cons] at h; omega) := by - cases n <;> simp - theorem get_tail (l : List α) (i) (h : i < l.tail.length) (h' : i + 1 < l.length := (by simp only [length_tail] at h; omega)) : l.tail.get ⟨i, h⟩ = l.get ⟨i + 1, h'⟩ := by diff --git a/Mathlib/Data/List/Chain.lean b/Mathlib/Data/List/Chain.lean index 74ed472f6b59f3..f209731a712cec 100644 --- a/Mathlib/Data/List/Chain.lean +++ b/Mathlib/Data/List/Chain.lean @@ -421,7 +421,7 @@ theorem Chain'.cons_of_le [LinearOrder α] {a : α} {as m : List α} cases as with | nil => simp only [le_iff_lt_or_eq, reduceCtorEq, or_false] at hmas - exact (List.Lex.not_nil_right (·<·) _ hmas).elim + exact (List.not_lt_nil _ hmas).elim | cons a' as => rw [List.chain'_cons] at ha refine gt_of_gt_of_ge ha.1 ?_ @@ -431,7 +431,7 @@ theorem Chain'.cons_of_le [LinearOrder α] {a : α} {as m : List α} rw [← not_le] at hmas apply hmas apply le_of_lt - exact (List.lt_iff_lex_lt _ _).mp (List.lt.head _ _ hh) + exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel hh) · simp_all only [List.cons.injEq, le_refl] lemma Chain'.chain {α : Type*} {R : α → α → Prop} {l : List α} {v : α} diff --git a/Mathlib/Data/List/Lemmas.lean b/Mathlib/Data/List/Lemmas.lean index ef62ad8d898a98..f9ef0d4e07c183 100644 --- a/Mathlib/Data/List/Lemmas.lean +++ b/Mathlib/Data/List/Lemmas.lean @@ -17,17 +17,9 @@ variable {α β γ : Type*} namespace List -@[simp] -theorem length_flatMap (l : List α) (f : α → List β) : - length (List.flatMap l f) = sum (map (length ∘ f) l) := by - rw [List.flatMap, length_flatten, map_map] - -lemma countP_flatMap (p : β → Bool) (l : List α) (f : α → List β) : - countP p (l.flatMap f) = sum (map (countP p ∘ f) l) := by - rw [List.flatMap, countP_flatten, map_map] - -lemma count_flatMap [BEq β] (l : List α) (f : α → List β) (x : β) : - count x (l.flatMap f) = sum (map (count x ∘ f) l) := countP_flatMap _ _ _ +set_option linter.deprecated false in +@[simp, deprecated "No deprecation message was provided." (since := "2024-10-17")] +lemma Nat.sum_eq_listSum (l : List ℕ) : Nat.sum l = l.sum := rfl @[deprecated (since := "2024-08-20")] alias getElem_reverse' := getElem_reverse diff --git a/Mathlib/Data/List/Lex.lean b/Mathlib/Data/List/Lex.lean index 69566d9aa5d915..4c166bc4b024a9 100644 --- a/Mathlib/Data/List/Lex.lean +++ b/Mathlib/Data/List/Lex.lean @@ -35,24 +35,13 @@ variable {α : Type u} /-! ### lexicographic ordering -/ - -/-- Given a strict order `<` on `α`, the lexicographic strict order on `List α`, for which -`[a0, ..., an] < [b0, ..., b_k]` if `a0 < b0` or `a0 = b0` and `[a1, ..., an] < [b1, ..., bk]`. -The definition is given for any relation `r`, not only strict orders. -/ -inductive Lex (r : α → α → Prop) : List α → List α → Prop - | nil {a l} : Lex r [] (a :: l) - | cons {a l₁ l₂} (h : Lex r l₁ l₂) : Lex r (a :: l₁) (a :: l₂) - | rel {a₁ l₁ a₂ l₂} (h : r a₁ a₂) : Lex r (a₁ :: l₁) (a₂ :: l₂) - namespace Lex theorem cons_iff {r : α → α → Prop} [IsIrrefl α r] {a l₁ l₂} : Lex r (a :: l₁) (a :: l₂) ↔ Lex r l₁ l₂ := ⟨fun h => by cases' h with _ _ _ _ _ h _ _ _ _ h; exacts [h, (irrefl_of r a h).elim], Lex.cons⟩ -@[simp] -theorem not_nil_right (r : α → α → Prop) (l : List α) : ¬Lex r l [] := - nofun +@[deprecated (since := "2024-12-21")] alias not_nil_right := not_lex_nil theorem nil_left_or_eq_nil {r : α → α → Prop} (l : List α) : List.Lex r [] l ∨ l = [] := match l with @@ -158,9 +147,6 @@ end Lex instance LT' [LT α] : LT (List α) := ⟨Lex (· < ·)⟩ -theorem nil_lt_cons [LT α] (a : α) (l : List α) : [] < a :: l := - Lex.nil - instance [LinearOrder α] : LinearOrder (List α) := linearOrderOfSTO (Lex (· < ·)) @@ -168,25 +154,8 @@ instance [LinearOrder α] : LinearOrder (List α) := instance LE' [LinearOrder α] : LE (List α) := Preorder.toLE -theorem lt_iff_lex_lt [LinearOrder α] (l l' : List α) : lt l l' ↔ Lex (· < ·) l l' := by - constructor <;> - intro h - · induction h with - | nil b bs => exact Lex.nil - | @head a as b bs hab => apply Lex.rel; assumption - | @tail a as b bs hab hba _ ih => - have heq : a = b := _root_.le_antisymm (le_of_not_lt hba) (le_of_not_lt hab) - subst b; apply Lex.cons; assumption - · induction h with - | @nil a as => apply lt.nil - | @cons a as bs _ ih => apply lt.tail <;> simp [ih] - | @rel a as b bs h => apply lt.head; assumption - -@[simp] -theorem nil_le {α} [LinearOrder α] {l : List α} : [] ≤ l := - match l with - | [] => le_rfl - | _ :: _ => le_of_lt <| nil_lt_cons _ _ +theorem lt_iff_lex_lt [LinearOrder α] (l l' : List α) : List.lt l l' ↔ Lex (· < ·) l l' := by + rw [List.lt] theorem head_le_of_lt [Preorder α] {a a' : α} {l l' : List α} (h : (a' :: l') < (a :: l)) : a' ≤ a := diff --git a/Mathlib/Data/List/MinMax.lean b/Mathlib/Data/List/MinMax.lean index cb9db4834736d0..71564ef6cb8486 100644 --- a/Mathlib/Data/List/MinMax.lean +++ b/Mathlib/Data/List/MinMax.lean @@ -449,7 +449,7 @@ lemma getD_max?_eq_unbot'_maximum (l : List α) (d : α) : cases hz : l.max? with | none => simp [List.max?_eq_none_iff.mp hz] at hy | some z => - have : Std.Antisymm (α := α) (· ≤ ·) := ⟨_root_.le_antisymm⟩ + have : Std.Antisymm (α := α) (· ≤ ·) := ⟨fun _ _ => _root_.le_antisymm⟩ rw [List.max?_eq_some_iff] at hz · rw [Option.getD_some] exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left) diff --git a/Mathlib/Data/List/Permutation.lean b/Mathlib/Data/List/Permutation.lean index 49f6dd007cd72d..bdd3205fa2f21a 100644 --- a/Mathlib/Data/List/Permutation.lean +++ b/Mathlib/Data/List/Permutation.lean @@ -89,7 +89,7 @@ theorem map_permutationsAux2' {α' β'} (g : α → α') (g' : β → β') (t : induction' ys with ys_hd _ ys_ih generalizing f f' · simp · simp only [map, permutationsAux2_snd_cons, cons_append, cons.injEq] - rw [ys_ih, permutationsAux2_fst] + rw [ys_ih] · refine ⟨?_, rfl⟩ simp only [← map_cons, ← map_append]; apply H · intro a; apply H @@ -268,7 +268,7 @@ theorem length_permutationsAux : refine permutationsAux.rec (by simp) ?_ intro t ts is IH1 IH2 have IH2 : length (permutationsAux is nil) + 1 = is.length ! := by simpa using IH2 - simp only [factorial, Nat.mul_comm, add_eq] at IH1 + simp only [length, factorial, Nat.mul_comm, add_eq] at IH1 rw [permutationsAux_cons, length_foldr_permutationsAux2' _ _ _ _ _ fun l m => (perm_of_mem_permutations m).length_eq, permutations, length, length, IH2, Nat.succ_add, Nat.factorial_succ, Nat.mul_comm (_ + 1), @@ -387,7 +387,7 @@ theorem getElem_permutations'Aux (s : List α) (x : α) (n : ℕ) (hn : n < length (permutations'Aux x s)) : (permutations'Aux x s)[n] = s.insertIdx n x := by induction' s with y s IH generalizing n - · simp only [length, Nat.zero_add, Nat.lt_one_iff] at hn + · simp only [permutations'Aux, length, Nat.zero_add, lt_one_iff] at hn simp [hn] · cases n · simp [get] @@ -509,7 +509,7 @@ theorem nodup_permutations (s : List α) (hs : Nodup s) : Nodup s.permutations : lemma permutations_take_two (x y : α) (s : List α) : (x :: y :: s).permutations.take 2 = [x :: y :: s, y :: x :: s] := by - induction s <;> simp only [take, permutationsAux, permutationsAux.rec, permutationsAux2, id_eq] + induction s <;> simp [permutations, permutationsAux.rec] @[simp] theorem nodup_permutations_iff {s : List α} : Nodup s.permutations ↔ Nodup s := by diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean index cf9e742f04bfcc..c321ba243c9b5a 100644 --- a/Mathlib/Data/Nat/Bitwise.lean +++ b/Mathlib/Data/Nat/Bitwise.lean @@ -80,12 +80,9 @@ theorem binaryRec_of_ne_zero {C : Nat → Sort*} (z : C 0) (f : ∀ b n, C n → lemma bitwise_bit {f : Bool → Bool → Bool} (h : f false false = false := by rfl) (a m b n) : bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) := by conv_lhs => unfold bitwise - #adaptation_note /-- nightly-2024-03-16: simp was - -- simp (config := { unfoldPartialApp := true }) only [bit, bit1, bit0, Bool.cond_eq_ite] -/ simp only [bit, ite_apply, Bool.cond_eq_ite] - have h2 x : (x + x + 1) % 2 = 1 := by rw [← two_mul, add_comm]; apply add_mul_mod_self_left have h4 x : (x + x + 1) / 2 = x := by rw [← two_mul, add_comm]; simp [add_mul_div_left] - cases a <;> cases b <;> simp [h2, h4] <;> split_ifs + cases a <;> cases b <;> simp [h4] <;> split_ifs <;> simp_all +decide [two_mul] lemma bit_mod_two_eq_zero_iff (a x) : diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean index 1e19ccb7c114d7..5f52c3eb53cf2b 100644 --- a/Mathlib/Data/Nat/Defs.lean +++ b/Mathlib/Data/Nat/Defs.lean @@ -978,15 +978,12 @@ lemma mod_two_ne_zero : n % 2 ≠ 0 ↔ n % 2 = 1 := mod_two_not_eq_zero lemma div_mod_eq_mod_mul_div (a b c : ℕ) : a / b % c = a % (b * c) / b := (mod_mul_right_div_self a b c).symm -/-- Variant of `Nat.lt_div_iff_mul_lt` (added in Lean 4.16) that assumes `d ∣ n`. -/ +/-- Variant of `Nat.lt_div_iff_mul_lt` that assumes `d ∣ n`. -/ protected lemma lt_div_iff_mul_lt' (hdn : d ∣ n) (a : ℕ) : a < n / d ↔ d * a < n := by obtain rfl | hd := d.eq_zero_or_pos · simp [Nat.zero_dvd.1 hdn] · rw [← Nat.mul_lt_mul_left hd, ← Nat.eq_mul_of_div_eq_right hdn rfl] -@[deprecated Nat.lt_div_iff_mul_lt' (since := "2024-12-29")] -protected alias lt_div_iff_mul_lt := Nat.lt_div_iff_mul_lt' - lemma mul_div_eq_iff_dvd {n d : ℕ} : d * (n / d) = n ↔ d ∣ n := calc d * (n / d) = n ↔ d * (n / d) = d * (n / d) + (n % d) := by rw [div_add_mod] diff --git a/Mathlib/Data/Num/Basic.lean b/Mathlib/Data/Num/Basic.lean index 54c9466d8c3121..25e1a56167888d 100644 --- a/Mathlib/Data/Num/Basic.lean +++ b/Mathlib/Data/Num/Basic.lean @@ -138,7 +138,7 @@ def ofNatSucc : ℕ → PosNum def ofNat (n : ℕ) : PosNum := ofNatSucc (Nat.pred n) -instance {n : ℕ} : OfNat PosNum (n + 1) where +instance (priority := low) {n : ℕ} : OfNat PosNum (n + 1) where ofNat := ofNat (n + 1) open Ordering diff --git a/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean b/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean index 284cbecc9b9255..02db3344da144e 100644 --- a/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean +++ b/Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean @@ -309,7 +309,7 @@ def Fix.drec {β : Fix F α → Type u} rw [Fix.rec_eq] dsimp simp? [appendFun_id_id] at ih says - simp only [appendFun_id_id, MvFunctor.id_map] at ih + simp only [appendFun_id_id, MvFunctor.id_map, y] at ih congr conv => rhs diff --git a/Mathlib/Data/String/Basic.lean b/Mathlib/Data/String/Basic.lean index b4a8b44ddfbf83..7bd4035fff1aa3 100644 --- a/Mathlib/Data/String/Basic.lean +++ b/Mathlib/Data/String/Basic.lean @@ -28,10 +28,12 @@ def ltb (s₁ s₂ : Iterator) : Bool := else true else false +/-- This overrides an instance in core Lean. -/ instance LT' : LT String := ⟨fun s₁ s₂ ↦ ltb s₁.iter s₂.iter⟩ -instance decidableLT : DecidableRel (α := String) (· < ·) := by +/-- This instance has a prime to avoid the name of the corresponding instance in core Lean. -/ +instance decidableLT' : DecidableRel (α := String) (· < ·) := by simp only [LT'] infer_instance -- short-circuit type class inference diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean index 8e81475a4c4926..7f7f4602004bc0 100644 --- a/Mathlib/Data/Vector/Basic.lean +++ b/Mathlib/Data/Vector/Basic.lean @@ -317,7 +317,7 @@ This lemma is the `cons` version of `scanl_get`. @[simp] theorem scanl_cons (x : α) : scanl f b (x ::ᵥ v) = b ::ᵥ scanl f (f b x) v := by simp only [scanl, toList_cons, List.scanl]; dsimp - simp only [cons]; rfl + simp only [cons] /-- The underlying `List` of a `Vector` after a `scanl` is the `List.scanl` of the underlying `List` of the original `Vector`. @@ -351,8 +351,7 @@ theorem scanl_head : (scanl f b v).head = b := by · have : v = nil := by simp only [eq_iff_true_of_subsingleton] simp only [this, scanl_nil, head_cons] · rw [← cons_head_tail v] - simp only [← get_zero, get_eq_get_toList, toList_scanl, toList_cons, List.scanl, Fin.val_zero, - List.get] + simp [← get_zero, get_eq_get_toList] /-- For an index `i : Fin n`, the nth element of `scanl` of a vector `v : Vector α n` at `i.succ`, is equal to the application diff --git a/Mathlib/Deprecated/LazyList.lean b/Mathlib/Deprecated/LazyList.lean index 04f7bd5f25dc52..80dbb7f596a7a6 100644 --- a/Mathlib/Deprecated/LazyList.lean +++ b/Mathlib/Deprecated/LazyList.lean @@ -102,7 +102,7 @@ instance : LawfulMonad LazyList := LawfulMonad.mk' (bind_pure_comp := by intro _ _ f xs simp only [bind, Functor.map, pure, singleton] - induction xs using LazyList.traverse.induct (m := @Id) (f := f) with + induction xs using LazyList.traverse.induct with | case1 => simp only [Thunk.pure, LazyList.bind, LazyList.traverse, Id.pure_eq] | case2 _ _ ih => diff --git a/Mathlib/FieldTheory/Finite/GaloisField.lean b/Mathlib/FieldTheory/Finite/GaloisField.lean index f2ef367ab073ba..e4a08ea36a9377 100644 --- a/Mathlib/FieldTheory/Finite/GaloisField.lean +++ b/Mathlib/FieldTheory/Finite/GaloisField.lean @@ -112,7 +112,9 @@ theorem finrank {n} (h : n ≠ 0) : Module.finrank (ZMod p) (GaloisField p n) = intro x hx -- We discharge the `p = 0` separately, to avoid typeclass issues on `ZMod p`. cases p; cases hp - refine Subring.closure_induction ?_ ?_ ?_ ?_ ?_ ?_ hx <;> simp_rw [mem_rootSet_of_ne aux] + simp only [g_poly] at aux + refine Subring.closure_induction ?_ ?_ ?_ ?_ ?_ ?_ hx + <;> simp_rw [mem_rootSet_of_ne aux] · rintro x (⟨r, rfl⟩ | hx) · simp only [g_poly, map_sub, map_pow, aeval_X] rw [← map_pow, ZMod.pow_card_pow, sub_self] diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean index 4606e2f6b56925..e00f5ad914dd07 100644 --- a/Mathlib/Lean/Expr/Basic.lean +++ b/Mathlib/Lean/Expr/Basic.lean @@ -199,7 +199,7 @@ def eraseProofs (e : Expr) : MetaM Expr := Meta.transform (skipConstInApp := true) e (pre := fun e => do if (← Meta.isProof e) then - return .continue (← mkSyntheticSorry (← inferType e)) + return .continue (← mkSorry (← inferType e) true) else return .continue) diff --git a/Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean b/Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean index 18f7876c84b897..2abc81e56ab46d 100644 --- a/Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean +++ b/Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean @@ -100,7 +100,7 @@ where goArray (as bs : Array DTExpr) : StateM (Std.HashMap MVarId MVarId) Bool := do if h : as.size = bs.size then for g : i in [:as.size] do - unless ← go as[i] (bs[i]'(h ▸ g.2)) do + unless ← go as[i] (bs[i]'(h ▸ g.2.1)) do return false return true else diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index c9f988704f257f..b8ca669106157f 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -794,7 +794,7 @@ theorem _root_.mem_span_of_iInf_ker_le_ker [Finite ι] {L : ι → E →ₗ[𝕜 let L' i : (E ⧸ p) →ₗ[𝕜] 𝕜 := p.liftQ (L i) (iInf_le _ i) let K' : (E ⧸ p) →ₗ[𝕜] 𝕜 := p.liftQ K h have : ⨅ i, ker (L' i) ≤ ker K' := by - simp_rw [← ker_pi, L', pi_liftQ_eq_liftQ_pi, ker_liftQ_eq_bot' p φ p_eq] + simp_rw +zetaDelta [← ker_pi, pi_liftQ_eq_liftQ_pi, ker_liftQ_eq_bot' p φ p_eq] exact bot_le obtain ⟨c, hK'⟩ := (mem_span_range_iff_exists_fun 𝕜).1 (FiniteDimensional.mem_span_of_iInf_ker_le_ker this) diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean index aa5849bf7df418..973a47eec399b1 100644 --- a/Mathlib/LinearAlgebra/LinearIndependent.lean +++ b/Mathlib/LinearAlgebra/LinearIndependent.lean @@ -1366,10 +1366,10 @@ lemma exists_linearIndependent' (v : ι → V) : have hs {i : ι} (hi : i ∈ s) : v i ∈ t := by obtain ⟨a, rfl⟩ := hi; simp [hf] let f' (a : s) : t := ⟨v a.val, hs a.property⟩ refine ⟨s, Subtype.val, Subtype.val_injective, hsp.symm ▸ by congr; aesop, ?_⟩ - · rw [← show Subtype.val ∘ f' = v ∘ Subtype.val by ext; simp] + · rw [← show Subtype.val ∘ f' = v ∘ Subtype.val by ext; simp [f']] apply hli.comp rintro ⟨i, x, rfl⟩ ⟨j, y, rfl⟩ hij - simp only [Subtype.ext_iff, hf] at hij + simp only [Subtype.ext_iff, hf, f'] at hij simp [hij] variable {K t} diff --git a/Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean b/Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean index e6d05239e63241..72c3fbee941ce6 100644 --- a/Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/SemiringInverse.lean @@ -122,7 +122,7 @@ theorem mul_adjp_apply_ne (h : i ≠ j) : (A * adjp 1 A) i j = (A * adjp (-1) A) have key : ({j}ᶜ : Finset n) = disjUnion ({i} : Finset n) ({i, j} : Finset n)ᶜ (by simp) := by rw [singleton_disjUnion, cons_eq_insert, compl_insert, insert_erase] rwa [mem_compl, mem_singleton] - simp_rw [key, prod_disjUnion, prod_singleton, Perm.mul_apply, swap_apply_left, ← mul_assoc] + simp_rw [key, prod_disjUnion, prod_singleton, f, Perm.mul_apply, swap_apply_left, ← mul_assoc] rw [mul_comm (A i x) (A i (σ i)), hp.2.2] refine congr_arg _ (prod_congr rfl fun x hx ↦ ?_) rw [mem_compl, mem_insert, mem_singleton, not_or] at hx diff --git a/Mathlib/Logic/Basic.lean b/Mathlib/Logic/Basic.lean index d63de1913084e4..409b30a71b81e0 100644 --- a/Mathlib/Logic/Basic.lean +++ b/Mathlib/Logic/Basic.lean @@ -478,7 +478,7 @@ than `forall_swap`. -/ theorem imp_forall_iff {α : Type*} {p : Prop} {q : α → Prop} : (p → ∀ x, q x) ↔ ∀ x, p → q x := forall_swap -@[simp] lemma imp_forall_iff_forall (A : Prop) (B : A → Prop) : +lemma imp_forall_iff_forall (A : Prop) (B : A → Prop) : (A → ∀ h : A, B h) ↔ ∀ h : A, B h := by by_cases h : A <;> simp [h] theorem exists_swap {p : α → β → Prop} : (∃ x y, p x y) ↔ ∃ y x, p x y := diff --git a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean index 7dbef7d0668220..a88490002c8be2 100644 --- a/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean +++ b/Mathlib/MeasureTheory/Integral/FundThmCalculus.lean @@ -1193,7 +1193,7 @@ lemma integral_unitInterval_deriv_eq_sub [RCLike 𝕜] [NormedSpace 𝕜 E] [IsS simp only [one_smul] exact this.const_add z₀ convert (integral_eq_sub_of_hasDerivAt hderiv' hint) using 1 - · simp_rw [← integral_smul, Function.comp_apply] + · simp_rw [← integral_smul, Function.comp_apply, γ] · simp only [γ, Function.comp_apply, one_smul, zero_smul, add_zero] /-! diff --git a/Mathlib/MeasureTheory/Integral/Marginal.lean b/Mathlib/MeasureTheory/Integral/Marginal.lean index 483452c38db137..69a96847de886b 100644 --- a/Mathlib/MeasureTheory/Integral/Marginal.lean +++ b/Mathlib/MeasureTheory/Integral/Marginal.lean @@ -124,7 +124,7 @@ theorem lmarginal_singleton (f : (∀ i, π i) → ℝ≥0∞) (i : δ) : = ∫⁻ (y : π (default : α)), f (updateFinset x {i} (e y)) ∂μ (default : α) := by simp_rw [lmarginal, measurePreserving_piUnique (fun j : ({i} : Finset δ) ↦ μ j) |>.symm _ - |>.lintegral_map_equiv] + |>.lintegral_map_equiv, e, α] _ = ∫⁻ xᵢ, f (Function.update x i xᵢ) ∂μ i := by simp [update_eq_updateFinset]; rfl variable {μ} in diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean index 01e220cf30c659..26c5afe1429816 100644 --- a/Mathlib/ModelTheory/Semantics.lean +++ b/Mathlib/ModelTheory/Semantics.lean @@ -323,7 +323,7 @@ theorem realize_iff : (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Reali simp only [BoundedFormula.iff, realize_inf, realize_imp, and_imp, ← iff_def] theorem realize_castLE_of_eq {m n : ℕ} (h : m = n) {h' : m ≤ n} {φ : L.BoundedFormula α m} - {v : α → M} {xs : Fin n → M} : (φ.castLE h').Realize v xs ↔ φ.Realize v (xs ∘ cast h) := by + {v : α → M} {xs : Fin n → M} : (φ.castLE h').Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h) := by subst h simp only [castLE_rfl, cast_refl, OrderIso.coe_refl, Function.comp_id] @@ -422,7 +422,7 @@ theorem realize_restrictFreeVar [DecidableEq α] {n : ℕ} {φ : L.BoundedFormul induction φ with | falsum => rfl | equal => - simp only [Realize, freeVarFinset.eq_2] + simp only [Realize, restrictFreeVar, freeVarFinset.eq_2] rw [realize_restrictVarLeft v' (by simp [hv']), realize_restrictVarLeft v' (by simp [hv'])] simp [Function.comp_apply] | rel => @@ -431,7 +431,7 @@ theorem realize_restrictFreeVar [DecidableEq α] {n : ℕ} {φ : L.BoundedFormul rw [realize_restrictVarLeft v' (by simp [hv'])] simp [Function.comp_apply] | imp _ _ ih1 ih2 => - simp only [Realize, freeVarFinset.eq_4] + simp only [Realize, restrictFreeVar, freeVarFinset.eq_4] rw [ih1, ih2] <;> simp [hv'] | all _ ih3 => simp only [restrictFreeVar, Realize] diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean index 8e39a25fbcd576..b44c36b5a8f8e1 100644 --- a/Mathlib/NumberTheory/Bernoulli.lean +++ b/Mathlib/NumberTheory/Bernoulli.lean @@ -291,7 +291,7 @@ theorem sum_range_pow (n p : ℕ) : simp only [f, exp_pow_eq_rescale_exp, rescale, one_div, coeff_mk, RingHom.coe_mk, coeff_exp, RingHom.id_apply, cast_mul, Algebra.id.map_eq_id] -- manipulate factorials and binomial coefficients - simp? at h says simp only [succ_eq_add_one, mem_range] at h + simp? at h says simp only [succ_eq_add_one, mem_range, f] at h rw [choose_eq_factorial_div_factorial h.le, eq_comm, div_eq_iff (hne q.succ), succ_eq_add_one, mul_assoc _ _ (q.succ ! : ℚ), mul_comm _ (q.succ ! : ℚ), ← mul_assoc, div_mul_eq_mul_div] simp only [add_eq, add_zero, IsUnit.mul_iff, Nat.isUnit_iff, succ.injEq, cast_mul, diff --git a/Mathlib/NumberTheory/Modular.lean b/Mathlib/NumberTheory/Modular.lean index 8b2189779e182e..8d3b0be4e59061 100644 --- a/Mathlib/NumberTheory/Modular.lean +++ b/Mathlib/NumberTheory/Modular.lean @@ -478,7 +478,10 @@ theorem c_eq_zero (hz : z ∈ 𝒟ᵒ) (hg : g • z ∈ 𝒟ᵒ) : g 1 0 = 0 := by_contra hc let a := g' 0 0 let d := g' 1 1 - have had : T ^ (-a) * g' = S * T ^ d := by rw [g_eq_of_c_eq_one hc]; group + have had : T ^ (-a) * g' = S * T ^ d := by + rw [g_eq_of_c_eq_one hc] + dsimp [a, d] + group let w := T ^ (-a) • g' • z have h₁ : w = S • T ^ d • z := by simp only [w, ← mul_smul, had] replace h₁ : normSq w < 1 := h₁.symm ▸ normSq_S_smul_lt_one (one_lt_normSq_T_zpow_smul hz d) diff --git a/Mathlib/Order/Fin/Basic.lean b/Mathlib/Order/Fin/Basic.lean index 10983f1527c033..4e47785db09e5b 100644 --- a/Mathlib/Order/Fin/Basic.lean +++ b/Mathlib/Order/Fin/Basic.lean @@ -122,7 +122,7 @@ end FromFin /-! #### Monotonicity -/ lemma val_strictMono : StrictMono (val : Fin n → ℕ) := fun _ _ ↦ id -lemma cast_strictMono {k l : ℕ} (h : k = l) : StrictMono (cast h) := fun {_ _} h ↦ h +lemma cast_strictMono {k l : ℕ} (h : k = l) : StrictMono (Fin.cast h) := fun {_ _} h ↦ h lemma strictMono_succ : StrictMono (succ : Fin n → Fin (n + 1)) := fun _ _ ↦ succ_lt_succ lemma strictMono_castLE (h : n ≤ m) : StrictMono (castLE h : Fin n → Fin m) := fun _ _ ↦ id @@ -182,7 +182,7 @@ def orderIsoSubtype : Fin n ≃o {i // i < n} := `castOrderIso eq i` embeds `i` into an equal `Fin` type. -/ @[simps] def castOrderIso (eq : n = m) : Fin n ≃o Fin m where - toEquiv := ⟨cast eq, cast eq.symm, leftInverse_cast eq, rightInverse_cast eq⟩ + toEquiv := ⟨Fin.cast eq, Fin.cast eq.symm, leftInverse_cast eq, rightInverse_cast eq⟩ map_rel_iff' := cast_le_cast eq @[deprecated (since := "2024-05-23")] alias castIso := castOrderIso diff --git a/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean b/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean index bf904f8bef341a..d19605f9b549be 100644 --- a/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean +++ b/Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean @@ -326,8 +326,7 @@ theorem natAbs_det_equiv (I : Ideal S) {E : Type*} [EquivLike E S I] [AddEquivCl -- which maps `(S ⧸ I)` to `Π i, ZMod (a i).nat_abs`. haveI : ∀ i, NeZero (a i).natAbs := fun i => ⟨Int.natAbs_ne_zero.mpr (Ideal.smithCoeffs_ne_zero b I hI i)⟩ - simp_rw [Nat.card_congr (Ideal.quotientEquivPiZMod I b hI).toEquiv, Nat.card_pi, - Nat.card_zmod] + simp_rw [Nat.card_congr (Ideal.quotientEquivPiZMod I b hI).toEquiv, Nat.card_pi, Nat.card_zmod, a] /-- Let `b` be a basis for `S` over `ℤ` and `bI` a basis for `I` over `ℤ` of the same dimension. Then an alternative way to compute the norm of `I` is given by taking the determinant of `bI` diff --git a/Mathlib/RingTheory/Kaehler/JacobiZariski.lean b/Mathlib/RingTheory/Kaehler/JacobiZariski.lean index dba3d8955d2518..d4c5b8c6ef68f2 100644 --- a/Mathlib/RingTheory/Kaehler/JacobiZariski.lean +++ b/Mathlib/RingTheory/Kaehler/JacobiZariski.lean @@ -135,7 +135,7 @@ lemma Cotangent.exact : have hz : z.1 ∈ P.ker.map (Q.toComp P).toAlgHom.toRingHom := e have : Extension.Cotangent.mk (P := (Q.comp P).toExtension) ⟨x, hx'⟩ = Extension.Cotangent.mk z := by - ext; simpa only [comp_vars, val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two] + ext; simpa only [comp_vars, val_mk, Ideal.toCotangent_eq, sub_sub_cancel, pow_two, z] rw [this, ← Submodule.restrictScalars_mem (Q.comp P).Ring, ← Submodule.mem_comap, ← Submodule.span_singleton_le_iff_mem, ← Submodule.map_le_map_iff_of_injective (f := Submodule.subtype _) Subtype.val_injective, Submodule.map_subtype_span_singleton, diff --git a/Mathlib/RingTheory/Polynomial/Chebyshev.lean b/Mathlib/RingTheory/Polynomial/Chebyshev.lean index 24c2e98c66aa76..394b556910dccc 100644 --- a/Mathlib/RingTheory/Polynomial/Chebyshev.lean +++ b/Mathlib/RingTheory/Polynomial/Chebyshev.lean @@ -81,7 +81,7 @@ protected theorem induct (motive : ℤ → Prop) (add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)) (neg_add_one : ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)) : ∀ (a : ℤ), motive a := - T.induct Unit motive zero one add_two fun n hn hnm => by + T.induct motive zero one add_two fun n hn hnm => by simpa only [Int.negSucc_eq, neg_add] using neg_add_one n hn hnm @[simp] diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean index 9d8409124777ab..9d81bb8ff98acd 100644 --- a/Mathlib/SetTheory/Ordinal/Notation.lean +++ b/Mathlib/SetTheory/Ordinal/Notation.lean @@ -64,10 +64,11 @@ def omega : ONote := oadd 1 1 0 /-- The ordinal denoted by a notation -/ -@[simp] noncomputable def repr : ONote → Ordinal.{0} | 0 => 0 | oadd e n a => ω ^ repr e * n + repr a +@[simp] theorem repr_zero : repr 0 = 0 := rfl +attribute [simp] repr.eq_1 repr.eq_2 /-- Print `ω^s*n`, omitting `s` if `e = 0` or `e = 1`, and omitting `n` if `n = 1` -/ private def toString_aux (e : ONote) (n : ℕ) (s : String) : String := @@ -112,8 +113,7 @@ instance : WellFoundedRelation ONote := ⟨(· < ·), InvImage.wf repr Ordinal.lt_wf⟩ /-- Convert a `Nat` into an ordinal -/ -@[coe] -def ofNat : ℕ → ONote +@[coe] def ofNat : ℕ → ONote | 0 => 0 | Nat.succ n => oadd 0 n.succPNat 0 @@ -126,17 +126,14 @@ def ofNat : ℕ → ONote @[simp] theorem ofNat_succ (n) : ofNat (Nat.succ n) = oadd 0 n.succPNat 0 := rfl -instance nat (n : ℕ) : OfNat ONote n where +instance (priority := low) nat (n : ℕ) : OfNat ONote n where ofNat := ofNat n -@[simp 1200] -theorem ofNat_one : ofNat 1 = 1 := - rfl +@[simp 1200] theorem ofNat_one : ofNat 1 = 1 := rfl -@[simp] -theorem repr_ofNat (n : ℕ) : repr (ofNat n) = n := by cases n <;> simp +@[simp] theorem repr_ofNat (n : ℕ) : repr (ofNat n) = n := by cases n <;> simp -theorem repr_one : repr (ofNat 1) = (1 : ℕ) := repr_ofNat 1 +@[simp] theorem repr_one : repr 1 = (1 : ℕ) := repr_ofNat 1 theorem omega0_le_oadd (e n a) : ω ^ repr e ≤ repr (oadd e n a) := by refine le_trans ?_ (le_add_right _ _) @@ -174,8 +171,7 @@ theorem eq_of_cmp_eq : ∀ {o₁ o₂}, cmp o₁ o₂ = Ordering.eq → o₁ = o simp protected theorem zero_lt_one : (0 : ONote) < 1 := by - simp only [lt_def, repr, opow_zero, Nat.succPNat_coe, Nat.cast_one, mul_one, add_zero, - zero_lt_one] + simp only [lt_def, repr_zero, repr_one, Nat.cast_one, zero_lt_one] /-- `NFBelow o b` says that `o` is a normal form ordinal notation satisfying `repr o < ω ^ b`. -/ inductive NFBelow : ONote → Ordinal.{0} → Prop @@ -442,7 +438,7 @@ theorem repr_add : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ + o₂) = rep conv at nf => simp [HAdd.hAdd, Add.add] conv in _ + o => simp [HAdd.hAdd, Add.add] cases' h : add a o with e' n' a' <;> - simp only [Add.add, add, addAux, h'.symm, h, add_assoc, repr] at nf h₁ ⊢ + simp only [Add.add, add, addAux, h'.symm, h, add_assoc, repr_zero, repr] at nf h₁ ⊢ have := h₁.fst; haveI := nf.fst; have ee := cmp_compares e e' cases he : cmp e e' <;> simp only [he, Ordering.compares_gt, Ordering.compares_lt, Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢ @@ -568,7 +564,7 @@ theorem repr_mul : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ * o₂) = rep simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos _ omega0_pos).2 (Nat.cast_le.2 n₁.2) by_cases e0 : e₂ = 0 · cases' Nat.exists_eq_succ_of_ne_zero n₂.ne_zero with x xe - simp only [e0, repr, PNat.mul_coe, natCast_mul, opow_zero, one_mul] + simp only [Mul.mul, mul, e0, ↓reduceIte, repr, PNat.mul_coe, natCast_mul, opow_zero, one_mul] simp only [xe, h₂.zero_of_zero e0, repr, add_zero] rw [natCast_succ x, add_mul_succ _ ao, mul_assoc] · simp only [repr] @@ -658,8 +654,7 @@ theorem split_eq_scale_split' : ∀ {o o' m} [NF o], split' o = (o', m) → spli simp only [split_eq_scale_split' h', and_imp] have : 1 + (e - 1) = e := by refine repr_inj.1 ?_ - simp only [repr_add, repr, opow_zero, Nat.succPNat_coe, Nat.cast_one, mul_one, add_zero, - repr_sub] + simp only [repr_add, repr_one, Nat.cast_one, repr_sub] have := mt repr_inj.1 e0 exact Ordinal.add_sub_cancel_of_le <| one_le_iff_ne_zero.2 this intros @@ -684,10 +679,9 @@ theorem nf_repr_split' : ∀ {o o' m} [NF o], split' o = (o', m) → NF o' ∧ r have := mt repr_inj.1 e0 rw [← opow_add, Ordinal.add_sub_cancel_of_le (one_le_iff_ne_zero.2 this)] refine ⟨NF.oadd (by infer_instance) _ ?_, ?_⟩ - · simp at this ⊢ - refine - IH₁.below_of_lt' - ((Ordinal.mul_lt_mul_iff_left omega0_pos).1 <| lt_of_le_of_lt (le_add_right _ m') ?_) + · simp only [opow_one, repr_sub, repr_one, Nat.cast_one] at this ⊢ + refine IH₁.below_of_lt' + ((Ordinal.mul_lt_mul_iff_left omega0_pos).1 <| lt_of_le_of_lt (le_add_right _ m') ?_) rw [← this, ← IH₂] exact h.snd'.repr_lt · rw [this] @@ -717,8 +711,7 @@ theorem nf_repr_split {o o' m} [NF o] (h : split o = (o', m)) : NF o' ∧ repr o cases' nf_repr_split' e with s₁ s₂ rw [split_eq_scale_split' e] at h injection h; substs o' n - simp only [repr_scale, repr, opow_zero, Nat.succPNat_coe, Nat.cast_one, mul_one, add_zero, - opow_one, s₂.symm, and_true] + simp only [repr_scale, repr_one, Nat.cast_one, opow_one, ← s₂, and_true] infer_instance theorem split_dvd {o o' m} [NF o] (h : split o = (o', m)) : ω ∣ repr o' := by @@ -900,7 +893,7 @@ theorem repr_opow (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o · cases' e₂ : split' o₂ with b' k cases' nf_repr_split' e₂ with _ r₂ by_cases h : m = 0 - · simp [opow_def, opow, e₁, h, r₁, e₂, r₂] + · simp [opowAux2, opow_def, opow, e₁, h, r₁, e₂, r₂] simp only [opow_def, opowAux2, opow, e₁, h, r₁, e₂, r₂, repr, opow_zero, Nat.succPNat_coe, Nat.cast_succ, Nat.cast_zero, _root_.zero_add, mul_one, add_zero, one_opow, npow_eq_pow] @@ -924,16 +917,13 @@ theorem repr_opow (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o simp only [opow_def, opow, e₁, r₁, split_eq_scale_split' e₂, opowAux2, repr] cases' k with k · simp [r₂, opow_mul, repr_opow_aux₁ a00 al aa, add_assoc] - · simp? [r₂, opow_add, opow_mul, mul_assoc, add_assoc, -repr, -opow_natCast] says - simp only [mulNat_eq_mul, repr_add, repr_scale, repr_mul, repr_ofNat, opow_add, opow_mul, - mul_assoc, add_assoc, r₂, Nat.cast_add, Nat.cast_one, add_one_eq_succ, opow_succ] - simp only [repr, opow_zero, Nat.succPNat_coe, Nat.cast_one, mul_one, add_zero, opow_one] + · simp [opow, opowAux2, r₂, opow_add, opow_mul, mul_assoc, add_assoc] rw [repr_opow_aux₁ a00 al aa, scale_opowAux] - simp only [repr_mul, repr_scale, repr, opow_zero, Nat.succPNat_coe, Nat.cast_one, mul_one, + simp only [repr_mul, repr_scale, repr, opow_zero, PNat.val_ofNat, Nat.cast_one, mul_one, add_zero, opow_one, opow_mul] rw [← mul_add, ← add_assoc ((ω : Ordinal.{0}) ^ repr a0 * (n : ℕ))] congr 1 - rw [← opow_succ] + rw [← pow_succ, ← opow_natCast, ← opow_natCast] exact (repr_opow_aux₂ _ ad a00 al _ _).2 /-- Given an ordinal, returns: diff --git a/Mathlib/Tactic.lean b/Mathlib/Tactic.lean index 7938e6809683b7..86cf871b98d367 100644 --- a/Mathlib/Tactic.lean +++ b/Mathlib/Tactic.lean @@ -68,7 +68,6 @@ import Mathlib.Tactic.DefEqTransformations import Mathlib.Tactic.DeprecateTo import Mathlib.Tactic.DeriveCountable import Mathlib.Tactic.DeriveFintype -import Mathlib.Tactic.DeriveToExpr import Mathlib.Tactic.DeriveTraversable import Mathlib.Tactic.Eqns import Mathlib.Tactic.Eval diff --git a/Mathlib/Tactic/CC/Addition.lean b/Mathlib/Tactic/CC/Addition.lean index 6e7a9fe150ad21..4ad4dc22d38f02 100644 --- a/Mathlib/Tactic/CC/Addition.lean +++ b/Mathlib/Tactic/CC/Addition.lean @@ -398,8 +398,8 @@ equality `r*a = s*b`. -/ def superposeAC (ts a : ACApps) (tsEqa : DelayedExpr) : CCM Unit := do let .apps op args := ts | return for hi : i in [:args.size] do - if i == 0 || (args[i]'hi.2) != (args[i - 1]'(Nat.lt_of_le_of_lt (i.sub_le 1) hi.2)) then - let some ent := (← get).acEntries.find? (args[i]'hi.2) | failure + if i == 0 || args[i] != (args[i - 1]'(Nat.lt_of_le_of_lt (i.sub_le 1) hi.2.1)) then + let some ent := (← get).acEntries.find? args[i] | failure let occs := ent.RLHSOccs for tr in occs do let .apps optr _ := tr | continue @@ -607,7 +607,7 @@ partial def internalizeAppLit (e : Expr) : CCM Unit := do pinfo := (← getFunInfoNArgs fn apps.size).paramInfo.toList if state.hoFns.isSome && fn.isConst && !(state.hoFns.iget.contains fn.constName) then for h : i in [:apps.size] do - let arg := (apps[i]'h.2).appArg! + let arg := apps[i].appArg! addOccurrence e arg false if pinfo.head?.any ParamInfo.isInstImplicit then -- We do not recurse on instances when `(← get).config.ignoreInstances` is `true`. @@ -625,13 +625,13 @@ partial def internalizeAppLit (e : Expr) : CCM Unit := do -- Expensive case where we store a quadratic number of occurrences, -- as described in the paper "Congruence Closure in Internsional Type Theory" for h : i in [:apps.size] do - let curr := apps[i]'h.2 + let curr := apps[i] let .app currFn currArg := curr | unreachable! if i < apps.size - 1 then mkEntry curr false for h : j in [i:apps.size] do - addOccurrence (apps[j]'h.2) currArg false - addOccurrence (apps[j]'h.2) currFn false + addOccurrence apps[j] currArg false + addOccurrence apps[j] currFn false if pinfo.head?.any ParamInfo.isInstImplicit then -- We do not recurse on instances when `(← get).config.ignoreInstances` is `true`. mkEntry currArg false diff --git a/Mathlib/Tactic/CC/Datatypes.lean b/Mathlib/Tactic/CC/Datatypes.lean index d45f190596b926..c83766cd0e41bc 100644 --- a/Mathlib/Tactic/CC/Datatypes.lean +++ b/Mathlib/Tactic/CC/Datatypes.lean @@ -583,10 +583,10 @@ def getVarWithLeastOccs (ccs : CCState) (e : ACApps) (inLHS : Bool) : Option Exp let mut r := args[0]? let mut numOccs := r.casesOn 0 fun r' => ccs.getNumROccs r' inLHS for hi : i in [1:args.size] do - if (args[i]'hi.2) != (args[i - 1]'(Nat.lt_of_le_of_lt (i.sub_le 1) hi.2)) then - let currOccs := ccs.getNumROccs (args[i]'hi.2) inLHS + if args[i] != (args[i - 1]'(Nat.lt_of_le_of_lt (i.sub_le 1) hi.2.1)) then + let currOccs := ccs.getNumROccs args[i] inLHS if currOccs < numOccs then - r := (args[i]'hi.2) + r := args[i] numOccs := currOccs return r | .ofExpr e => e diff --git a/Mathlib/Tactic/CC/MkProof.lean b/Mathlib/Tactic/CC/MkProof.lean index c3827b0526b161..5f17a75846cc5a 100644 --- a/Mathlib/Tactic/CC/MkProof.lean +++ b/Mathlib/Tactic/CC/MkProof.lean @@ -73,7 +73,7 @@ partial def isCongruent (e₁ e₂ : Expr) : CCM Bool := do e₂.withApp fun f₂ args₂ => do if ha : args₁.size = args₂.size then for hi : i in [:args₁.size] do - if (← getRoot (args₁[i]'hi.2)) != (← getRoot (args₂[i]'(ha.symm ▸ hi.2))) then + if (← getRoot args₁[i]) != (← getRoot (args₂[i]'(ha.symm ▸ hi.2.1))) then return false if f₁ == f₂ then return true else if (← getRoot f₁) != (← getRoot f₂) then @@ -289,13 +289,13 @@ partial def mkCongrProofCore (lhs rhs : Expr) (heqProofs : Bool) : CCM Expr := d let mut lemmaArgs : Array Expr := #[] for hi : i in [:lhsArgs.size] do guard !kindsIt.isEmpty - lemmaArgs := lemmaArgs.push (lhsArgs[i]'hi.2) |>.push (rhsArgs[i]'(ha.symm ▸ hi.2)) + lemmaArgs := lemmaArgs.push lhsArgs[i] |>.push (rhsArgs[i]'(ha.symm ▸ hi.2.1)) if kindsIt[0]! matches CongrArgKind.heq then - let some p ← getHEqProof (lhsArgs[i]'hi.2) (rhsArgs[i]'(ha.symm ▸ hi.2)) | failure + let some p ← getHEqProof lhsArgs[i] (rhsArgs[i]'(ha.symm ▸ hi.2.1)) | failure lemmaArgs := lemmaArgs.push p else guard (kindsIt[0]! matches .eq) - let some p ← getEqProof (lhsArgs[i]'hi.2) (rhsArgs[i]'(ha.symm ▸ hi.2)) | failure + let some p ← getEqProof lhsArgs[i] (rhsArgs[i]'(ha.symm ▸ hi.2.1)) | failure lemmaArgs := lemmaArgs.push p kindsIt := kindsIt.eraseIdx! 0 let mut r := mkAppN specLemma.proof lemmaArgs @@ -606,8 +606,8 @@ expression. -/ def simplifyACStep (e : ACApps) : CCM (Option (ACApps × DelayedExpr)) := do if let .apps _ args := e then for h : i in [:args.size] do - if i == 0 || (args[i]'h.2) != (args[i - 1]'(Nat.lt_of_le_of_lt (i.sub_le 1) h.2)) then - let some ae := (← get).acEntries.find? (args[i]'h.2) | failure + if i == 0 || args[i] != (args[i - 1]'(Nat.lt_of_le_of_lt (i.sub_le 1) h.2.1)) then + let some ae := (← get).acEntries.find? args[i] | failure let occs := ae.RLHSOccs let mut Rlhs? : Option ACApps := none for Rlhs in occs do diff --git a/Mathlib/Tactic/Common.lean b/Mathlib/Tactic/Common.lean index b59d768f32d0c3..00ceda6c80a6d7 100644 --- a/Mathlib/Tactic/Common.lean +++ b/Mathlib/Tactic/Common.lean @@ -13,7 +13,6 @@ import Plausible import ImportGraph.Imports -- Import common Batteries tactics and commands -import Batteries.Tactic.Where import Batteries.Tactic.Basic import Batteries.Tactic.HelpCmd @@ -47,7 +46,6 @@ import Mathlib.Tactic.Conv import Mathlib.Tactic.Convert import Mathlib.Tactic.DefEqTransformations import Mathlib.Tactic.DeprecateTo -import Mathlib.Tactic.DeriveToExpr import Mathlib.Tactic.Eqns import Mathlib.Tactic.ExistsI import Mathlib.Tactic.ExtractGoal diff --git a/Mathlib/Tactic/DeriveToExpr.lean b/Mathlib/Tactic/DeriveToExpr.lean deleted file mode 100644 index d82a0df118816e..00000000000000 --- a/Mathlib/Tactic/DeriveToExpr.lean +++ /dev/null @@ -1,230 +0,0 @@ -/- -Copyright (c) 2023 Kyle Miller. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kyle Miller --/ -import Lean.Elab.Deriving.Ord -import Mathlib.Tactic.ToLevel - -/-! -# A `ToExpr` derive handler - -This module defines a `ToExpr` derive handler for inductive types. It supports mutually inductive -types as well. - -The `ToExpr` derive handlers support universe level polymorphism. This is implemented using the -`Lean.ToLevel` class. To use `ToExpr` in places where there is universe polymorphism, make sure -to have a `[ToLevel.{u}]` instance available. - -**Warning:** Import `Mathlib.Tactic.ToExpr` instead of this one. This ensures that you are using -the universe polymorphic `ToExpr` instances that override the ones from Lean 4 core. - -Implementation note: this derive handler was originally modeled after the `Repr` derive handler. --/ - -namespace Mathlib.Deriving.ToExpr - -open Lean Elab Lean.Parser.Term -open Meta Command Deriving - -/-- Specialization of `Lean.Elab.Deriving.mkHeader` for `ToExpr`. -/ -def mkToExprHeader (indVal : InductiveVal) : TermElabM Header := do - -- The auxiliary functions we produce are `indtype -> Expr`. - let header ← mkHeader ``ToExpr 1 indVal - return header - -/-- Give a term that is equivalent to `(term| mkAppN $f #[$args,*])`. -As an optimization, `mkAppN` is pre-expanded out to use `Expr.app` directly. -/ -def mkAppNTerm (f : Term) (args : Array Term) : MetaM Term := - args.foldlM (fun a b => `(Expr.app $a $b)) f - -/-- Create the body of the `toExpr` function -for the `ToExpr` instance, which is a `match` expression -that calls `toExpr` and `toTypeExpr` to assemble an expression for a given term. -For recursive inductive types, `auxFunName` refers to the `ToExpr` instance -for the current type. -For mutually recursive types, we rely on the local instances set up by `mkLocalInstanceLetDecls`. -/ -def mkToExprBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) : - TermElabM Term := do - let discrs ← mkDiscrs header indVal - let alts ← mkAlts - `(match $[$discrs],* with $alts:matchAlt*) -where - /-- Create the `match` cases, one per constructor. -/ - mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do - let mut alts := #[] - for ctorName in indVal.ctors do - let ctorInfo ← getConstInfoCtor ctorName - let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do - let mut patterns := #[] - -- add `_` pattern for indices - for _ in [:indVal.numIndices] do - patterns := patterns.push (← `(_)) - let mut ctorArgs := #[] - let mut rhsArgs : Array Term := #[] - let mkArg (x : Expr) (a : Term) : TermElabM Term := do - if (← inferType x).isAppOf indVal.name then - `($(mkIdent auxFunName) $a) - else if ← Meta.isType x then - `(toTypeExpr $a) - else - `(toExpr $a) - -- add `_` pattern for inductive parameters, which are inaccessible - for i in [:ctorInfo.numParams] do - let a := mkIdent header.argNames[i]! - ctorArgs := ctorArgs.push (← `(_)) - rhsArgs := rhsArgs.push <| ← mkArg xs[i]! a - for i in [:ctorInfo.numFields] do - let a := mkIdent (← mkFreshUserName `a) - ctorArgs := ctorArgs.push a - rhsArgs := rhsArgs.push <| ← mkArg xs[ctorInfo.numParams + i]! a - patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs:term*)) - let levels ← indVal.levelParams.toArray.mapM (fun u => `(toLevel.{$(mkIdent u)})) - let rhs : Term ← - mkAppNTerm (← `(Expr.const $(quote ctorInfo.name) [$levels,*])) rhsArgs - `(matchAltExpr| | $[$patterns:term],* => $rhs) - alts := alts.push alt - return alts - -/-- Create the body of the `toTypeExpr` function for the `ToExpr` instance. -Calls `toExpr` and `toTypeExpr` to the arguments to the type constructor. -/ -def mkToTypeExpr (argNames : Array Name) (indVal : InductiveVal) : TermElabM Term := do - let levels ← indVal.levelParams.toArray.mapM (fun u => `(toLevel.{$(mkIdent u)})) - forallTelescopeReducing indVal.type fun xs _ => do - let mut args : Array Term := #[] - for i in [:xs.size] do - let x := xs[i]! - let a := mkIdent argNames[i]! - if ← Meta.isType x then - args := args.push <| ← `(toTypeExpr $a) - else - args := args.push <| ← `(toExpr $a) - mkAppNTerm (← `((Expr.const $(quote indVal.name) [$levels,*]))) args - -/-- -For mutually recursive inductive types, the strategy is to have local `ToExpr` instances in scope -for each of the inductives when defining each instance. -This way, each instance can freely use `toExpr` and `toTypeExpr` for each of the other types. - -Note that each instance gets its own definition of each of the others' `toTypeExpr` fields. -(This is working around the fact that the `Deriving.Context` API assumes -that each instance in mutual recursion only has a single auxiliary definition. -There are other ways to work around it, but `toTypeExpr` implementations -are very simple, so duplicating them seemed to be OK.) -/ -def mkLocalInstanceLetDecls (ctx : Deriving.Context) (argNames : Array Name) : - TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do - let mut letDecls := #[] - for i in [:ctx.typeInfos.size] do - let indVal := ctx.typeInfos[i]! - let auxFunName := ctx.auxFunNames[i]! - let currArgNames ← mkInductArgNames indVal - let numParams := indVal.numParams - let currIndices := currArgNames[numParams:] - let binders ← mkImplicitBinders currIndices - let argNamesNew := argNames[:numParams] ++ currIndices - let indType ← mkInductiveApp indVal argNamesNew - let instName ← mkFreshUserName `localinst - let toTypeExpr ← mkToTypeExpr argNames indVal - let letDecl ← `(Parser.Term.letDecl| $(mkIdent instName):ident $binders:implicitBinder* : - ToExpr $indType := - { toExpr := $(mkIdent auxFunName), toTypeExpr := $toTypeExpr }) - letDecls := letDecls.push letDecl - return letDecls - -/-- Fix the output of `mkInductiveApp` to explicitly reference universe levels. -/ -def fixIndType (indVal : InductiveVal) (t : Term) : TermElabM Term := - match t with - | `(@$f $args*) => - let levels := indVal.levelParams.toArray.map mkIdent - `(@$f.{$levels,*} $args*) - | _ => throwError "(internal error) expecting output of `mkInductiveApp`" - -/-- Make `ToLevel` instance binders for all the level variables. -/ -def mkToLevelBinders (indVal : InductiveVal) : TermElabM (TSyntaxArray ``instBinderF) := do - indVal.levelParams.toArray.mapM (fun u => `(instBinderF| [ToLevel.{$(mkIdent u)}])) - -open TSyntax.Compat in -/-- Make a `toExpr` function for the given inductive type. -The implementations of each `toExpr` function for a (mutual) inductive type -are given as top-level private definitions. -These end up being assembled into `ToExpr` instances in `mkInstanceCmds`. -For mutual inductive types, -then each of the other types' `ToExpr` instances are provided as local instances, -to wire together the recursion (this necessitates these auxiliary definitions being `partial`). -/ -def mkAuxFunction (ctx : Deriving.Context) (i : Nat) : TermElabM Command := do - let auxFunName := ctx.auxFunNames[i]! - let indVal := ctx.typeInfos[i]! - let header ← mkToExprHeader indVal - let mut body ← mkToExprBody header indVal auxFunName - if ctx.usePartial then - let letDecls ← mkLocalInstanceLetDecls ctx header.argNames - body ← mkLet letDecls body - -- We need to alter the last binder (the one for the "target") to have explicit universe levels - -- so that the `ToLevel` instance arguments can use them. - let addLevels binder := - match binder with - | `(bracketedBinderF| ($a : $ty)) => do `(bracketedBinderF| ($a : $(← fixIndType indVal ty))) - | _ => throwError "(internal error) expecting inst binder" - let binders := header.binders.pop - ++ (← mkToLevelBinders indVal) - ++ #[← addLevels header.binders.back!] - let levels := indVal.levelParams.toArray.map mkIdent - if ctx.usePartial then - `(private partial def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* : - Expr := $body:term) - else - `(private def $(mkIdent auxFunName):ident.{$levels,*} $binders:bracketedBinder* : - Expr := $body:term) - -/-- Create all the auxiliary functions using `mkAuxFunction` for the (mutual) inductive type(s). -Wraps the resulting definition commands in `mutual ... end`. -/ -def mkMutualBlock (ctx : Deriving.Context) : TermElabM Syntax := do - let mut auxDefs := #[] - for i in [:ctx.typeInfos.size] do - auxDefs := auxDefs.push (← mkAuxFunction ctx i) - `(mutual $auxDefs:command* end) - -open TSyntax.Compat in -/-- Assuming all of the auxiliary definitions exist, create all the `instance` commands -for the `ToExpr` instances for the (mutual) inductive type(s). -/ -def mkInstanceCmds (ctx : Deriving.Context) (typeNames : Array Name) : - TermElabM (Array Command) := do - let mut instances := #[] - for i in [:ctx.typeInfos.size] do - let indVal := ctx.typeInfos[i]! - if typeNames.contains indVal.name then - let auxFunName := ctx.auxFunNames[i]! - let argNames ← mkInductArgNames indVal - let binders ← mkImplicitBinders argNames - let binders := binders ++ (← mkInstImplicitBinders ``ToExpr indVal argNames) - let binders := binders ++ (← mkToLevelBinders indVal) - let indType ← fixIndType indVal (← mkInductiveApp indVal argNames) - let toTypeExpr ← mkToTypeExpr argNames indVal - let levels := indVal.levelParams.toArray.map mkIdent - let instCmd ← `(instance $binders:implicitBinder* : ToExpr $indType where - toExpr := $(mkIdent auxFunName).{$levels,*} - toTypeExpr := $toTypeExpr) - instances := instances.push instCmd - return instances - -/-- Returns all the commands generated by `mkMutualBlock` and `mkInstanceCmds`. -/ -def mkToExprInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do - let ctx ← mkContext "toExpr" declNames[0]! - let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx declNames) - trace[Elab.Deriving.toExpr] "\n{cmds}" - return cmds - -/-- The main entry point to the `ToExpr` derive handler. -/ -def mkToExprInstanceHandler (declNames : Array Name) : CommandElabM Bool := do - if (← declNames.allM isInductive) && declNames.size > 0 then - let cmds ← liftTermElabM <| mkToExprInstanceCmds declNames - cmds.forM elabCommand - return true - else - return false - -initialize - registerDerivingHandler ``Lean.ToExpr mkToExprInstanceHandler - registerTraceClass `Elab.Deriving.toExpr - -end Mathlib.Deriving.ToExpr diff --git a/Mathlib/Tactic/ITauto.lean b/Mathlib/Tactic/ITauto.lean index f87cbcddd6ec36..f9e460c2a588f3 100644 --- a/Mathlib/Tactic/ITauto.lean +++ b/Mathlib/Tactic/ITauto.lean @@ -6,7 +6,6 @@ Authors: Mario Carneiro import Batteries.Tactic.Exact import Batteries.Tactic.Init import Mathlib.Logic.Basic -import Mathlib.Tactic.DeriveToExpr import Mathlib.Util.AtomM import Qq diff --git a/Mathlib/Tactic/Linarith/Frontend.lean b/Mathlib/Tactic/Linarith/Frontend.lean index a63112c459afff..e76aaf4acb162e 100644 --- a/Mathlib/Tactic/Linarith/Frontend.lean +++ b/Mathlib/Tactic/Linarith/Frontend.lean @@ -223,7 +223,7 @@ abbrev ExprMultiMap α := Array (Expr × List α) (If the key is not in the map it returns `self.size` as the index.) -/ def ExprMultiMap.find {α : Type} (self : ExprMultiMap α) (k : Expr) : MetaM (Nat × List α) := do for h : i in [:self.size] do - let (k', vs) := self[i]'h.2 + let (k', vs) := self[i] if ← isDefEq k' k then return (i, vs) return (self.size, []) @@ -233,7 +233,7 @@ in the map. -/ def ExprMultiMap.insert {α : Type} (self : ExprMultiMap α) (k : Expr) (v : α) : MetaM (ExprMultiMap α) := do for h : i in [:self.size] do - if ← isDefEq (self[i]'h.2).1 k then + if ← isDefEq self[i].1 k then return self.modify i fun (k, vs) => (k, v::vs) return self.push (k, [v]) diff --git a/Mathlib/Tactic/Linter/FlexibleLinter.lean b/Mathlib/Tactic/Linter/FlexibleLinter.lean index f4ad7305528d77..f2a568cca5b344 100644 --- a/Mathlib/Tactic/Linter/FlexibleLinter.lean +++ b/Mathlib/Tactic/Linter/FlexibleLinter.lean @@ -295,7 +295,7 @@ def flexible : Std.HashSet Name := `Mathlib.Tactic.normNum, `linarith, `nlinarith, - ``Lean.Parser.Tactic.tacticNorm_cast_, + ``Lean.Parser.Tactic.tacticNorm_cast__, `Aesop.Frontend.Parser.aesopTactic, `Mathlib.Tactic.Tauto.tauto, `Mathlib.Meta.FunProp.funPropTacStx, diff --git a/Mathlib/Tactic/Linter/HaveLetLinter.lean b/Mathlib/Tactic/Linter/HaveLetLinter.lean index b88a5344a4265a..299b1766d115f4 100644 --- a/Mathlib/Tactic/Linter/HaveLetLinter.lean +++ b/Mathlib/Tactic/Linter/HaveLetLinter.lean @@ -49,10 +49,9 @@ register_option linter.haveLet : Nat := { namespace haveLet /-- find the `have` syntax. -/ -partial def isHave? : Syntax → Bool | .node _ ``Lean.Parser.Tactic.tacticHave_ _ => true - |_ => false + | _ => false end haveLet diff --git a/Mathlib/Tactic/SuccessIfFailWithMsg.lean b/Mathlib/Tactic/SuccessIfFailWithMsg.lean index 3881cd09cfd2ca..b3ef1a312fae91 100644 --- a/Mathlib/Tactic/SuccessIfFailWithMsg.lean +++ b/Mathlib/Tactic/SuccessIfFailWithMsg.lean @@ -29,7 +29,7 @@ syntax (name := successIfFailWithMsg) "success_if_fail_with_msg " term:max tacti /-- Evaluates `tacs` and succeeds only if `tacs` both fails and throws an error equal (as a string) to `msg`. -/ def successIfFailWithMessage {s α : Type} {m : Type → Type} - [Monad m] [MonadLiftT IO m] [MonadBacktrack s m] [MonadError m] + [Monad m] [MonadLiftT BaseIO m] [MonadBacktrack s m] [MonadError m] (msg : String) (tacs : m α) (ref : Option Syntax := none) : m Unit := do let s ← saveState let err ← diff --git a/Mathlib/Tactic/ToExpr.lean b/Mathlib/Tactic/ToExpr.lean index 89978007295321..72f4fd3b7ee873 100644 --- a/Mathlib/Tactic/ToExpr.lean +++ b/Mathlib/Tactic/ToExpr.lean @@ -3,50 +3,12 @@ Copyright (c) 2023 Kyle Miller. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Kyle Miller -/ -import Mathlib.Tactic.DeriveToExpr import Mathlib.Util.WhatsNew -/-! # `ToExpr` instances for Mathlib - -This module should be imported by any module that intends to define `ToExpr` instances. -It provides necessary dependencies (the `Lean.ToLevel` class) and it also overrides the instances -that come from core Lean 4 that do not handle universe polymorphism. -(See the module `Lean.ToExpr` for the instances that are overridden.) - -In addition, we provide some additional `ToExpr` instances for core definitions. +/-! +# `ToExpr` instances for Mathlib -/ -section override -- Note: this section uses `autoImplicit` pervasively -namespace Lean - -attribute [-instance] Lean.instToExprOption - -set_option autoImplicit true in -deriving instance ToExpr for Option - -attribute [-instance] Lean.instToExprList - -set_option autoImplicit true in -deriving instance ToExpr for List - -attribute [-instance] Lean.instToExprArray - -universe u in -instance {α : Type u} [ToExpr α] [ToLevel.{u}] : ToExpr (Array α) := - let type := toTypeExpr α - { toExpr := fun as => mkApp2 (mkConst ``List.toArray [toLevel.{u}]) type (toExpr as.toList) - toTypeExpr := mkApp (mkConst ``Array [toLevel.{u}]) type } - -attribute [-instance] Lean.instToExprProd - -set_option autoImplicit true in -deriving instance ToExpr for Prod - -deriving instance ToExpr for System.FilePath - -end Lean -end override - namespace Mathlib open Lean @@ -62,7 +24,6 @@ instance [ToLevel.{u}] : ToExpr PUnit.{u+1} where deriving instance ToExpr for String.Pos deriving instance ToExpr for Substring deriving instance ToExpr for SourceInfo -deriving instance ToExpr for Syntax.Preresolved deriving instance ToExpr for Syntax open DataValue in @@ -86,12 +47,10 @@ instance : ToExpr MData where toExpr := toExprMData toTypeExpr := mkConst ``MData -deriving instance ToExpr for FVarId deriving instance ToExpr for MVarId deriving instance ToExpr for LevelMVarId deriving instance ToExpr for Level deriving instance ToExpr for BinderInfo -deriving instance ToExpr for Literal deriving instance ToExpr for Expr end Mathlib diff --git a/Mathlib/Tactic/ToLevel.lean b/Mathlib/Tactic/ToLevel.lean index 17b243651eb54f..fd85a5198e967f 100644 --- a/Mathlib/Tactic/ToLevel.lean +++ b/Mathlib/Tactic/ToLevel.lean @@ -17,31 +17,6 @@ override the ones from Lean 4 core. namespace Lean -/-- A class to create `Level` expressions that denote particular universe levels in Lean. -`Lean.ToLevel.toLevel.{u}` evaluates to a `Lean.Level` term representing `u` -/ -@[pp_with_univ] -class ToLevel.{u} where - /-- A `Level` that represents the universe level `u`. -/ - toLevel : Level - /-- The universe itself. This is only here to avoid the "unused universe parameter" error. -/ - univ : Type u := Sort u -export ToLevel (toLevel) attribute [pp_with_univ] toLevel -instance : ToLevel.{0} where - toLevel := .zero - -universe u v - -instance [ToLevel.{u}] : ToLevel.{u+1} where - toLevel := .succ toLevel.{u} - -/-- `ToLevel` for `max u v`. This is not an instance since it causes divergence. -/ -def ToLevel.max [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{max u v} where - toLevel := .max toLevel.{u} toLevel.{v} - -/-- `ToLevel` for `imax u v`. This is not an instance since it causes divergence. -/ -def ToLevel.imax [ToLevel.{u}] [ToLevel.{v}] : ToLevel.{imax u v} where - toLevel := .imax toLevel.{u} toLevel.{v} - end Lean diff --git a/Mathlib/Topology/Category/Profinite/Nobeling.lean b/Mathlib/Topology/Category/Profinite/Nobeling.lean index 2af0c9f25bf29a..fc08069c2269f0 100644 --- a/Mathlib/Topology/Category/Profinite/Nobeling.lean +++ b/Mathlib/Topology/Category/Profinite/Nobeling.lean @@ -653,8 +653,7 @@ theorem GoodProducts.spanFin [WellFoundedLT I] : | cons b bs => apply le_of_lt rw [List.chain'_cons] at ha - have hlex := List.lt.head bs (b :: bs) ha.1 - exact (List.lt_iff_lex_lt _ _).mp hlex + exact (List.lt_iff_lex_lt _ _).mp (List.Lex.rel ha.1) end Fin @@ -783,7 +782,7 @@ def Products.nil : Products I := ⟨[], by simp only [List.chain'_nil]⟩ theorem Products.lt_nil_empty {I} [LinearOrder I] : { m : Products I | m < Products.nil } = ∅ := by ext ⟨m, hm⟩ refine ⟨fun h ↦ ?_, by tauto⟩ - simp only [Set.mem_setOf_eq, lt_iff_lex_lt, nil, List.Lex.not_nil_right] at h + simp only [Set.mem_setOf_eq, lt_iff_lex_lt, nil, List.not_lex_nil] at h instance {α : Type*} [TopologicalSpace α] [Nonempty α] : Nontrivial (LocallyConstant α ℤ) := ⟨0, 1, ne_of_apply_ne DFunLike.coe <| (Function.const_injective (β := ℤ)).ne zero_ne_one⟩ @@ -1588,7 +1587,7 @@ theorem chain'_cons_of_lt (l : MaxProducts C ho) refine lt_of_le_of_lt (Products.head!_le_of_lt hq (q.val.ne_nil_of_mem ha)) ?_ by_cases hM : l.val.Tail.val = [] · rw [Products.lt_iff_lex_lt, hM] at hq - simp only [List.Lex.not_nil_right] at hq + simp only [List.not_lex_nil] at hq · have := l.val.prop rw [max_eq_o_cons_tail C hsC ho l, List.chain'_iff_pairwise] at this exact List.rel_of_pairwise_cons this (List.head!_mem_self hM) diff --git a/MathlibTest/DeriveToExpr.lean b/MathlibTest/DeriveToExpr.lean index 54e4bae668ad1d..1fa2cb66f03381 100644 --- a/MathlibTest/DeriveToExpr.lean +++ b/MathlibTest/DeriveToExpr.lean @@ -1,4 +1,4 @@ -import Mathlib.Tactic.DeriveToExpr +import Lean namespace DeriveToExprTests open Lean @@ -57,7 +57,6 @@ instance {α : Type u} [ToExpr α] [ToLevel.{u+1}] : ToExpr (Bool → α) where deriving instance ToExpr for Bar -set_option linter.unusedTactic false in example : True := by run_tac do let f : Bool → Nat | false => 0 | true => 1 diff --git a/MathlibTest/HashCommandLinter.lean b/MathlibTest/HashCommandLinter.lean index 4193342406c141..cf5304e11e7345 100644 --- a/MathlibTest/HashCommandLinter.lean +++ b/MathlibTest/HashCommandLinter.lean @@ -2,6 +2,12 @@ import Lean.Elab.GuardMsgs import Mathlib.Tactic.AdaptationNote import Mathlib.Tactic.Linter.HashCommandLinter + +-- #adaptation_note +-- The hashCommand linter started failing after https://github.com/leanprover/lean4/pull/6299 +-- Disabling aync elaboration fixes it, but of course we're not going to do that globally. +set_option Elab.async false + set_option linter.hashCommand true section ignored_commands diff --git a/MathlibTest/HaveLetLinter.lean b/MathlibTest/HaveLetLinter.lean index ec7409b66ccded..96d2aae3e74e1b 100644 --- a/MathlibTest/HaveLetLinter.lean +++ b/MathlibTest/HaveLetLinter.lean @@ -1,6 +1,12 @@ import Mathlib.Tactic.Linter.HaveLetLinter import Mathlib.Tactic.Tauto + +-- #adaptation_note +-- The haveLet linter started failing after https://github.com/leanprover/lean4/pull/6299 +-- Disabling aync elaboration fixes it, but of course we're not going to do that globally. +set_option Elab.async false + set_option linter.haveLet 1 /-- diff --git a/MathlibTest/TransImports.lean b/MathlibTest/TransImports.lean index 964187009033dc..c2cc31e073e1f5 100644 --- a/MathlibTest/TransImports.lean +++ b/MathlibTest/TransImports.lean @@ -1,10 +1,10 @@ import Mathlib.Util.TransImports /-- -info: 'MathlibTest.TransImports' has at most 500 transitive imports +info: 'MathlibTest.TransImports' has at most 1000 transitive imports 3 starting with "Lean.Elab.I": [Lean.Elab.InfoTree, Lean.Elab.InfoTree.Main, Lean.Elab.InfoTree.Types] -/ #guard_msgs in -#trans_imports "Lean.Elab.I" at_most 500 +#trans_imports "Lean.Elab.I" at_most 1000 diff --git a/MathlibTest/toAdditive.lean b/MathlibTest/toAdditive.lean index a1f60be9190179..6e9807fa7979b7 100644 --- a/MathlibTest/toAdditive.lean +++ b/MathlibTest/toAdditive.lean @@ -424,7 +424,7 @@ run_cmd do unless findTranslation? (← getEnv) `localize.s == some `add_localize.s do throwError "3" /-- -warning: The source declaration one_eq_one was given the simp-attribute(s) reduce_mod_char, simp before calling @[to_additive]. The preferred method is to use something like `@[to_additive (attr := reduce_mod_char, simp)]` to apply the attribute to both one_eq_one and the target declaration zero_eq_zero. +warning: The source declaration one_eq_one was given the simp-attribute(s) simp, reduce_mod_char before calling @[to_additive]. The preferred method is to use something like `@[to_additive (attr := simp, reduce_mod_char)]` to apply the attribute to both one_eq_one and the target declaration zero_eq_zero. note: this linter can be disabled with `set_option linter.existingAttributeWarning false` -/ #guard_msgs in diff --git a/lake-manifest.json b/lake-manifest.json index b6975fa1f851e3..8a7f0e3ba49a25 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5", + "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155", "name": "plausible", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/LeanSearchClient", @@ -25,30 +25,30 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "9a0b533c2fbd6195df067630be18e11e4349051c", + "rev": "9cb79405471ae931ac718231d6299bfaffef9087", "name": "importGraph", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/ProofWidgets4", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2b000e02d50394af68cfb4770a291113d94801b5", + "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2", "name": "proofwidgets", "manifestFile": "lake-manifest.json", - "inputRev": "v0.0.48", + "inputRev": "v0.0.50", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/aesop", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2689851f387bb2cef351e6825fe94a56a304ca13", + "rev": "79402ad9ab4be9a2286701a9880697e2351e4955", "name": "aesop", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover-community/quote4", @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b", + "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c", "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "v4.15.0", + "inputRev": "v4.16.0-rc1", "inherited": false, "configFile": "lakefile.toml"}, {"url": "https://github.com/leanprover/lean4-cli", diff --git a/lakefile.lean b/lakefile.lean index 44bbb99b712510..a9a535eb971a2d 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,13 +7,13 @@ open Lake DSL ## Mathlib dependencies on upstream projects -/ -require "leanprover-community" / "batteries" @ git "v4.15.0" +require "leanprover-community" / "batteries" @ git "v4.16.0-rc1" require "leanprover-community" / "Qq" @ git "v4.15.0" -require "leanprover-community" / "aesop" @ git "v4.15.0" -require "leanprover-community" / "proofwidgets" @ git "v0.0.48" -require "leanprover-community" / "importGraph" @ git "v4.15.0" +require "leanprover-community" / "aesop" @ git "v4.16.0-rc1" +require "leanprover-community" / "proofwidgets" @ git "v0.0.50" +require "leanprover-community" / "importGraph" @ git "v4.16.0-rc1" require "leanprover-community" / "LeanSearchClient" @ git "main" -require "leanprover-community" / "plausible" @ git "v4.15.0" +require "leanprover-community" / "plausible" @ git "v4.16.0-rc1" /-! ## Options for building mathlib diff --git a/lean-toolchain b/lean-toolchain index d0eb99ff68d76c..62ccd7170eb943 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.15.0 +leanprover/lean4:v4.16.0-rc1 diff --git a/scripts/noshake.json b/scripts/noshake.json index 784455d70e40a0..8a935b90e4553c 100644 --- a/scripts/noshake.json +++ b/scripts/noshake.json @@ -90,7 +90,6 @@ "Mathlib.Tactic.Core", "Mathlib.Tactic.DefEqTransformations", "Mathlib.Tactic.DeriveFintype", - "Mathlib.Tactic.DeriveToExpr", "Mathlib.Tactic.Eqns", "Mathlib.Tactic.ExistsI", "Mathlib.Tactic.ExtendDoc", @@ -275,7 +274,6 @@ "Mathlib.Tactic.Positivity.Core"], "Mathlib.Tactic.FinCases": ["Mathlib.Data.Fintype.Basic"], "Mathlib.Tactic.Eval": ["Qq.Macro"], - "Mathlib.Tactic.DeriveToExpr": ["Lean.Elab.Deriving.Ord"], "Mathlib.Tactic.DeriveFintype": ["Mathlib.Data.Fintype.Basic", "Mathlib.Data.Fintype.Sigma", @@ -384,6 +382,8 @@ "Mathlib.Data.List.Range": ["Batteries.Data.Nat.Lemmas"], "Mathlib.Data.List.ProdSigma": ["Batteries.Data.Nat.Lemmas", "Mathlib.Data.List.Basic"], + "Mathlib.Data.List.Permutation": + ["Mathlib.Data.List.Flatten", "Mathlib.Data.List.Lemmas"], "Mathlib.Data.List.Lemmas": ["Mathlib.Data.List.InsertIdx"], "Mathlib.Data.List.Defs": ["Batteries.Data.RBMap.Basic"], "Mathlib.Data.List.Basic":