From 1aa54cff26e0e66316b1f34f6a6a60e1bdd3b665 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Thu, 9 Jul 2026 11:32:00 -0400 Subject: [PATCH 1/3] fix --- Archive/Imo/Imo1981Q3.lean | 2 +- Archive/Imo/Imo2024Q3.lean | 2 +- Mathlib/Algebra/Lie/LieTheorem.lean | 3 +-- Mathlib/Algebra/Polynomial/Derivative.lean | 2 +- Mathlib/Algebra/Polynomial/RuleOfSigns.lean | 2 +- Mathlib/Algebra/Polynomial/Sequence.lean | 2 +- Mathlib/Analysis/Analytic/Inverse.lean | 4 ++-- Mathlib/Analysis/Analytic/Uniqueness.lean | 2 +- Mathlib/Analysis/SpecificLimits/Normed.lean | 2 +- Mathlib/Combinatorics/Enumerative/Bell.lean | 4 +--- .../Combinatorics/SimpleGraph/Connectivity/Subgraph.lean | 2 +- Mathlib/Computability/Language.lean | 2 +- Mathlib/Data/Fin/Basic.lean | 4 ++-- Mathlib/Data/Fintype/Basic.lean | 2 +- Mathlib/Data/Fintype/Card.lean | 2 +- Mathlib/Data/Nat/Choose/Central.lean | 2 +- Mathlib/Data/Nat/Digits/Lemmas.lean | 2 +- Mathlib/Data/Nat/Init.lean | 6 +++--- Mathlib/Data/Nat/Nth.lean | 2 +- Mathlib/FieldTheory/IsRealClosed/Basic.lean | 2 +- Mathlib/FieldTheory/Separable.lean | 2 +- Mathlib/GroupTheory/GroupAction/Jordan.lean | 3 +-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean | 2 +- Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean | 2 +- Mathlib/LinearAlgebra/Finsupp/Pi.lean | 2 +- Mathlib/LinearAlgebra/Multilinear/Basic.lean | 2 +- .../ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean | 4 ++-- Mathlib/NumberTheory/Bernoulli.lean | 2 +- Mathlib/NumberTheory/BernoulliPolynomials.lean | 2 +- Mathlib/NumberTheory/DiophantineApproximation/Basic.lean | 2 +- .../ModularForms/LevelOne/DimensionFormula.lean | 4 ++-- Mathlib/NumberTheory/Pell.lean | 2 +- Mathlib/NumberTheory/Primorial.lean | 2 +- Mathlib/Order/Fin/Basic.lean | 2 +- Mathlib/Order/KrullDimension.lean | 2 +- Mathlib/RingTheory/AdjoinRoot.lean | 2 +- Mathlib/RingTheory/Etale/QuasiFinite.lean | 2 +- Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean | 2 +- Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean | 2 +- .../IntegralClosure/IsIntegral/AlmostIntegral.lean | 2 +- Mathlib/RingTheory/LittleWedderburn.lean | 2 +- Mathlib/RingTheory/Polynomial/Basic.lean | 4 ++-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean | 6 +++--- Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean | 2 +- Mathlib/RingTheory/Polynomial/IsIntegral.lean | 2 +- Mathlib/RingTheory/Polynomial/Nilpotent.lean | 2 +- Mathlib/RingTheory/Polynomial/Resultant/Basic.lean | 2 +- Mathlib/RingTheory/WittVector/Defs.lean | 2 +- Mathlib/RingTheory/WittVector/Frobenius.lean | 3 +-- Mathlib/RingTheory/WittVector/StructurePolynomial.lean | 2 +- Mathlib/RingTheory/ZariskisMainTheorem.lean | 5 ++--- Mathlib/Topology/Metrizable/Uniformity.lean | 2 +- 52 files changed, 62 insertions(+), 68 deletions(-) diff --git a/Archive/Imo/Imo1981Q3.lean b/Archive/Imo/Imo1981Q3.lean index 5ee39058bedb8c..99af9d0d1d0d35 100644 --- a/Archive/Imo/Imo1981Q3.lean +++ b/Archive/Imo/Imo1981Q3.lean @@ -109,7 +109,7 @@ Now we can use induction to show that solutions must be Fibonacci numbers. -/ theorem imp_fib {n : ℕ} (m : ℕ) (h : NatPredicate N m n) : ∃ k : ℕ, m = fib k ∧ n = fib (k + 1) := by - induction n using Nat.strong_induction_on generalizing m with | h n ih => ?_ + induction n using Nat.strong_induction_on generalizing m with | ind n ih have h3 : m ≤ n := h.m_le_n obtain (rfl : 1 = n) | (h4 : 1 < n) := (succ_le_iff.mpr h.n_pos).eq_or_lt · use 1 diff --git a/Archive/Imo/Imo2024Q3.lean b/Archive/Imo/Imo2024Q3.lean index 2c51652ba0ffd4..38431111d34572 100644 --- a/Archive/Imo/Imo2024Q3.lean +++ b/Archive/Imo/Imo2024Q3.lean @@ -193,7 +193,7 @@ lemma injOn_setOf_apply_add_one_eq_of_M_le {n : ℕ} (h : M a N ≤ n) : lemma empty_consecutive_apply_ge_M : {i | M a N ≤ a i ∧ M a N ≤ a (i + 1)} = ∅ := by rw [Set.eq_empty_iff_forall_notMem] intro i - induction i using Nat.strong_induction_on with | h i ih => + induction i using Nat.strong_induction_on with | ind i ih -- Let i be the first index where both `a i` and `a (i + 1)` are at least M. rintro ⟨hi1, hi2⟩ have hi : ∀ j < i, M a N ≤ a j → a (j + 1) < M a N := by simp_all diff --git a/Mathlib/Algebra/Lie/LieTheorem.lean b/Mathlib/Algebra/Lie/LieTheorem.lean index 99cfd0cfdef20b..7d83f6ca7eeb1e 100644 --- a/Mathlib/Algebra/Lie/LieTheorem.lean +++ b/Mathlib/Algebra/Lie/LieTheorem.lean @@ -126,8 +126,7 @@ private lemma weightSpaceOfIsLieTower_aux (z : L) (v : V) (hv : v ∈ weightSpac apply iSup_le intro i x hx simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero] - induction i using Nat.strong_induction_on generalizing x - next i ih => + induction i using Nat.strong_induction_on generalizing x | ind i ih obtain rfl | hi := eq_or_ne i 0 · simp_all [U'] obtain ⟨j, hj, hj'⟩ := key i hi diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean index 0005c6c05137f9..ae5372870034b9 100644 --- a/Mathlib/Algebra/Polynomial/Derivative.lean +++ b/Mathlib/Algebra/Polynomial/Derivative.lean @@ -202,7 +202,7 @@ theorem derivative_ofNat (n : ℕ) [n.AtLeastTwo] : theorem iterate_derivative_eq_zero {p : R[X]} {x : ℕ} (hx : p.natDegree < x) : Polynomial.derivative^[x] p = 0 := by - induction h : p.natDegree using Nat.strong_induction_on generalizing p x with | _ _ ih + induction h : p.natDegree using Nat.strong_induction_on generalizing p x with | ind _ ih subst h obtain ⟨t, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (pos_of_gt hx).ne' rw [Function.iterate_succ_apply] diff --git a/Mathlib/Algebra/Polynomial/RuleOfSigns.lean b/Mathlib/Algebra/Polynomial/RuleOfSigns.lean index 7cddfd744d4758..192a363667ab32 100644 --- a/Mathlib/Algebra/Polynomial/RuleOfSigns.lean +++ b/Mathlib/Algebra/Polynomial/RuleOfSigns.lean @@ -299,7 +299,7 @@ theorem succ_signVariations_le_X_sub_C_mul (hη : 0 < η) (hP : P ≠ 0) : signVariations P + 1 ≤ signVariations ((X - C η) * P) := by -- do induction on the degree generalize hd : P.natDegree = d - induction d using Nat.strong_induction_on generalizing P with | _ d ih => + induction d using Nat.strong_induction_on generalizing P with | ind d ih -- can assume it starts positive, otherwise negate P wlog h_lC : 0 < leadingCoeff P generalizing P with H · simpa using @H (-P) (by simpa) (by simpa) (by grind [leadingCoeff_eq_zero, leadingCoeff_neg]) diff --git a/Mathlib/Algebra/Polynomial/Sequence.lean b/Mathlib/Algebra/Polynomial/Sequence.lean index fa7c4361348825..7b9f36c893c627 100644 --- a/Mathlib/Algebra/Polynomial/Sequence.lean +++ b/Mathlib/Algebra/Polynomial/Sequence.lean @@ -99,7 +99,7 @@ lemma span_degreeLT {m : ℕ} (hCoeff : ∀ i < m, IsUnit (S i).leadingCoeff) : nontriviality R using Subsingleton.eq_zero P generalize hp : P.natDegree = n induction n using Nat.strong_induction_on generalizing P with - | h n ih => + | ind n ih => by_cases! p_ne_zero : P = 0 · simp [p_ne_zero] have hn : n < m := by diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean index 5a1ae3790ef0d7..5c17dfefba9369 100644 --- a/Mathlib/Analysis/Analytic/Inverse.lean +++ b/Mathlib/Analysis/Analytic/Inverse.lean @@ -85,7 +85,7 @@ series. -/ theorem leftInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.removeZero.leftInv i x = p.leftInv i x := by ext1 n - induction n using Nat.strong_induction_on with | _ n IH + induction n using Nat.strong_induction_on with | ind n IH match n with | 0 => simp -- if one replaces `simp` with `refl`, the proof times out in the kernel. | 1 => simp -- TODO: why? @@ -188,7 +188,7 @@ series. -/ theorem rightInv_removeZero (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) : p.removeZero.rightInv i x = p.rightInv i x := by ext1 n - induction n using Nat.strong_induction_on with | _ n IH + induction n using Nat.strong_induction_on with | ind n IH match n with | 0 => simp only [rightInv_coeff_zero] | 1 => simp only [rightInv_coeff_one] diff --git a/Mathlib/Analysis/Analytic/Uniqueness.lean b/Mathlib/Analysis/Analytic/Uniqueness.lean index c7842ff404e3fc..dfe5202d74d326 100644 --- a/Mathlib/Analysis/Analytic/Uniqueness.lean +++ b/Mathlib/Analysis/Analytic/Uniqueness.lean @@ -91,7 +91,7 @@ theorem Asymptotics.IsBigO.continuousMultilinearMap_apply_eq_zero {n : ℕ} {p : terms `p n (fun i ↦ y)` appearing in the sum are zero for any `n : ℕ`, `y : E`. -/ theorem HasFPowerSeriesAt.apply_eq_zero {p : FormalMultilinearSeries 𝕜 E F} {x : E} (h : HasFPowerSeriesAt 0 p x) (n : ℕ) : ∀ y : E, (p n fun _ => y) = 0 := by - refine Nat.strong_induction_on n fun k hk => ?_ + induction n using Nat.strong_induction_on with | ind k hk have psum_eq : p.partialSum (k + 1) = fun y => p k fun _ => y := by funext z refine Finset.sum_eq_single _ (fun b hb hnb => ?_) fun hn => ?_ diff --git a/Mathlib/Analysis/SpecificLimits/Normed.lean b/Mathlib/Analysis/SpecificLimits/Normed.lean index deecc84a1b3899..8559f4deffcf06 100644 --- a/Mathlib/Analysis/SpecificLimits/Normed.lean +++ b/Mathlib/Analysis/SpecificLimits/Normed.lean @@ -487,7 +487,7 @@ lemma summable_descFactorial_mul_geometric_of_norm_lt_one (k : ℕ) {r : R} (hr open Polynomial in theorem summable_pow_mul_geometric_of_norm_lt_one (k : ℕ) {r : R} (hr : ‖r‖ < 1) : Summable (fun n ↦ (n : R) ^ k * r ^ n : ℕ → R) := by - refine Nat.strong_induction_on k fun k hk => ?_ + induction k using Nat.strong_induction_on with | ind k hk obtain ⟨a, ha⟩ : ∃ (a : ℕ → ℕ), ∀ n, (n + k).descFactorial k = n ^ k + ∑ i ∈ range k, a i * n ^ i := by let P : Polynomial ℕ := (ascPochhammer ℕ k).comp (Polynomial.X + C 1) diff --git a/Mathlib/Combinatorics/Enumerative/Bell.lean b/Mathlib/Combinatorics/Enumerative/Bell.lean index b4a6ea99c6b401..9c73764437681f 100644 --- a/Mathlib/Combinatorics/Enumerative/Bell.lean +++ b/Mathlib/Combinatorics/Enumerative/Bell.lean @@ -254,9 +254,7 @@ private def sigmaPartitionWithPartEquiv (n : ℕ) : /-- `Nat.bell n` is equal to the sum of `Multiset.bell m` over all multisets `m : Multiset ℕ` such that `m.sum = n`. -/ theorem bell_eq_sum_partition (n : ℕ) : n.bell = ∑ p : n.Partition, p.parts.bell := by - refine Nat.strong_induction_on n ?_ - rintro (_ | n) ih - · simp + induction n using Nat.case_strong_induction_on with | hz => simp | hi n ih rw [Nat.bell_succ] calc _ = ∑ i ≤ n, ∑ q : (n - i).Partition, n.choose i * q.parts.bell := by diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean index aac973d31a57db..d108a8878959b6 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean @@ -495,7 +495,7 @@ lemma exists_mem_support_mem_erase_mem_support_takeUntil_eq_empty (s : Finset V) (h : {x ∈ s | x ∈ p.support}.Nonempty) : ∃ x ∈ s, ∃ hx : x ∈ p.support, {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} = ∅ := by simp only [← Finset.subset_empty] - induction hp : p.length + #s using Nat.strong_induction_on generalizing s v with | _ n ih + induction hp : p.length + #s using Nat.strong_induction_on generalizing s v with | ind n ih simp only [Finset.Nonempty, mem_filter] at h obtain ⟨x, hxs, hx⟩ := h obtain h | h := Finset.eq_empty_or_nonempty {t ∈ s.erase x | t ∈ (p.takeUntil x hx).support} diff --git a/Mathlib/Computability/Language.lean b/Mathlib/Computability/Language.lean index 292d3d1a7d69e1..1122fbbab98500 100644 --- a/Mathlib/Computability/Language.lean +++ b/Mathlib/Computability/Language.lean @@ -303,7 +303,7 @@ theorem self_eq_mul_add_iff {l m n : Language α} (hm : [] ∉ m) : l = m * l + mp h := by apply le_antisymm · intro x hx - induction hlen : x.length using Nat.strong_induction_on generalizing x with | _ _ ih + induction hlen : x.length using Nat.strong_induction_on generalizing x with | ind _ ih subst hlen rw [h] at hx obtain hx | hx := hx diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 344ac23ae0b0e3..3456d45fc4e203 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -462,11 +462,11 @@ section Rec @[elab_as_elim] lemma strong_induction_on {n : ℕ} {motive : Fin n → Prop} - (h : ∀ (j : Fin n) (_ : ∀ (k : Fin n), k < j → motive k), motive j) (i : Fin n) : + (ind : ∀ (j : Fin n) (ih : ∀ (k : Fin n), k < j → motive k), motive j) (i : Fin n) : motive i := by obtain ⟨i, hi⟩ := i induction i using Nat.strong_induction_on with - | h j hj => exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁) + | ind j hj => exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁) end Rec diff --git a/Mathlib/Data/Fintype/Basic.lean b/Mathlib/Data/Fintype/Basic.lean index 67f724a64a660c..5ec4d4ef84a20d 100644 --- a/Mathlib/Data/Fintype/Basic.lean +++ b/Mathlib/Data/Fintype/Basic.lean @@ -267,7 +267,7 @@ theorem exists_seq_of_forall_finset_exists {α : Type*} (P : α → Prop) (r : set f := seqOfForallFinsetExistsAux P r h' with hf have A : ∀ n : ℕ, P (f n) := by intro n - induction n using Nat.strong_induction_on with | _ n IH + induction n using Nat.strong_induction_on with | ind n IH have IH' : ∀ x : Fin n, P (f x) := fun n => IH n.1 n.2 rw [hf, seqOfForallFinsetExistsAux] exact diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean index 953def12af2219..876a34373260ab 100644 --- a/Mathlib/Data/Fintype/Card.lean +++ b/Mathlib/Data/Fintype/Card.lean @@ -488,7 +488,7 @@ theorem Fintype.induction_subsingleton_or_nontrivial {P : ∀ (α) [Fintype α], (∀ (β) [Fintype β], Fintype.card β < Fintype.card α → P β) → P α) : P α := by obtain ⟨n, hn⟩ : ∃ n, Fintype.card α = n := ⟨Fintype.card α, rfl⟩ - induction n using Nat.strong_induction_on generalizing α with | _ n ih + induction n using Nat.strong_induction_on generalizing α with | ind n ih rcases subsingleton_or_nontrivial α with hsing | hnontriv · apply hbase · apply hstep diff --git a/Mathlib/Data/Nat/Choose/Central.lean b/Mathlib/Data/Nat/Choose/Central.lean index 152abd2a21a3c1..af367fc31539a7 100644 --- a/Mathlib/Data/Nat/Choose/Central.lean +++ b/Mathlib/Data/Nat/Choose/Central.lean @@ -91,7 +91,7 @@ This bound is of interest because it appears in [Tochiori's refinement of Erdős's proof of Bertrand's postulate](tochiori_bertrand). -/ theorem four_pow_lt_mul_centralBinom (n : ℕ) (n_big : 4 ≤ n) : 4 ^ n < n * centralBinom n := by - induction n using Nat.strong_induction_on with | _ n IH + induction n using Nat.strong_induction_on with | ind n IH rcases lt_trichotomy n 4 with (hn | rfl | hn) · clear IH; exact False.elim ((not_lt.2 n_big) hn) · norm_num [centralBinom, choose] diff --git a/Mathlib/Data/Nat/Digits/Lemmas.lean b/Mathlib/Data/Nat/Digits/Lemmas.lean index b0ed2f0f1f05e1..cab160e6e6e93a 100644 --- a/Mathlib/Data/Nat/Digits/Lemmas.lean +++ b/Mathlib/Data/Nat/Digits/Lemmas.lean @@ -52,7 +52,7 @@ This section contains various lemmas of properties relating to `digits` and `ofD theorem length_digits (b n : ℕ) (hb : 1 < b) (hn : n ≠ 0) : (b.digits n).length = b.log n + 1 := by - induction n using Nat.strong_induction_on with | _ n IH + induction n using Nat.strong_induction_on with | ind n IH rw [digits_eq_cons_digits_div hb hn, List.length] by_cases h : n / b = 0 · simp [h] diff --git a/Mathlib/Data/Nat/Init.lean b/Mathlib/Data/Nat/Init.lean index cb4e7df684123e..c1136231310fe7 100644 --- a/Mathlib/Data/Nat/Init.lean +++ b/Mathlib/Data/Nat/Init.lean @@ -257,9 +257,9 @@ def stepInduction {motive : ℕ → Sort*} (k : ℕ) (base : ∀ i < k, motive i (show a - k + k = a by lia) ▸ step (a - k) fun _ _ ↦ stepInduction k base step _ @[elab_as_elim] -protected theorem strong_induction_on {p : ℕ → Prop} (n : ℕ) - (h : ∀ n, (∀ m < n, p m) → p n) : p n := - Nat.strongRecOn n h +protected theorem strong_induction_on {motive : ℕ → Prop} (n : ℕ) + (ind : ∀ n, (∀ m < n, motive m) → motive n) : motive n := + Nat.strongRecOn n ind protected theorem case_strong_induction_on {p : ℕ → Prop} (a : ℕ) (hz : p 0) (hi : ∀ n, (∀ m ≤ n, p m) → p (n + 1)) : p a := diff --git a/Mathlib/Data/Nat/Nth.lean b/Mathlib/Data/Nat/Nth.lean index 11e306887a5938..bc495125d97a62 100644 --- a/Mathlib/Data/Nat/Nth.lean +++ b/Mathlib/Data/Nat/Nth.lean @@ -290,7 +290,7 @@ lemma nth_le_of_strictMonoOn_of_mapsTo {p : ℕ → Prop} (f : ℕ → ℕ) (hmono : StrictMonoOn f { n : ℕ | ∀ hf : Set.Finite (setOf p), n < hf.toFinset.card }) {n : ℕ} : nth p n ≤ f n := by by_cases! hn : (∀ hf : Set.Finite (setOf p), n < hf.toFinset.card) - · induction n using Nat.strong_induction_on with | _ n ih => + · induction n using Nat.strong_induction_on with | ind n ih rw [nth_eq_sInf] refine csInf_le (by simp) ⟨hmaps hn, fun k hk => ?_⟩ have : f k < f n := by apply hmono <;> grind diff --git a/Mathlib/FieldTheory/IsRealClosed/Basic.lean b/Mathlib/FieldTheory/IsRealClosed/Basic.lean index 2b403d5c02ecde..fefe5729119bea 100644 --- a/Mathlib/FieldTheory/IsRealClosed/Basic.lean +++ b/Mathlib/FieldTheory/IsRealClosed/Basic.lean @@ -88,7 +88,7 @@ theorem exists_eq_zpow_of_odd (x : R) {k : ℤ} (hk : Odd k) : ∃ r, x = r ^ k theorem exists_eq_pow_of_isSquare {x : R} (hx : IsSquare x) {n : ℕ} (hn : n ≠ 0) : ∃ r, x = r ^ n := by induction n using Nat.strong_induction_on generalizing x with - | h n ih => + | ind n ih => rcases Nat.even_or_odd n with (even | odd) · rcases even with ⟨m, hm⟩ rcases hx with ⟨s, hs⟩ diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean index 6fe3e6458fa074..89bb0a459b1ac0 100644 --- a/Mathlib/FieldTheory/Separable.lean +++ b/Mathlib/FieldTheory/Separable.lean @@ -360,7 +360,7 @@ theorem separable_or {f : F[X]} (hf : Irreducible f) : theorem exists_separable_of_irreducible {f : F[X]} (hf : Irreducible f) (hp : p ≠ 0) : ∃ (n : ℕ) (g : F[X]), g.Separable ∧ expand F (p ^ n) g = f := by replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp - induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ N ih + induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | ind N ih rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩) · refine ⟨0, f, h, ?_⟩ rw [pow_zero, expand_one] diff --git a/Mathlib/GroupTheory/GroupAction/Jordan.lean b/Mathlib/GroupTheory/GroupAction/Jordan.lean index d0b05c2060d74a..2ca58b734c172b 100644 --- a/Mathlib/GroupTheory/GroupAction/Jordan.lean +++ b/Mathlib/GroupTheory/GroupAction/Jordan.lean @@ -111,8 +111,7 @@ theorem MulAction.IsPreprimitive.is_two_motive_of_is_motive → IsMultiplyPretransitive G α 2) ∧ (IsPreprimitive (fixingSubgroup G s) (ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2) := by - induction n using Nat.strong_induction_on generalizing α G with - | h n hrec => + induction n using Nat.strong_induction_on generalizing α G with | ind n hrec have : Finite α := Nat.finite_of_card_ne_zero <| ne_zero_of_lt hsn' have hs_ne_univ : s ≠ Set.univ := by intro hs diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean index a5247cb57e02cb..0b450d8a464f61 100644 --- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean +++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean @@ -84,7 +84,7 @@ open Nat @[to_additive] private theorem card_orderOf_eq_totient_aux₁ {d : ℕ} (hd : d ∣ Fintype.card α) (hpos : 0 < #{a : α | orderOf a = d}) : #{a : α | orderOf a = d} = φ d := by - induction d using Nat.strong_induction_on with | _ d IH + induction d using Nat.strong_induction_on with | ind d IH rcases Decidable.eq_or_ne d 0 with (rfl | hd0) · cases Fintype.card_ne_zero (eq_zero_of_zero_dvd hd) rcases Finset.card_pos.1 hpos with ⟨a, ha'⟩ diff --git a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean index 909bb28e8236b7..1cba10027b89ca 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean @@ -77,7 +77,7 @@ theorem iSup_maxGenEigenspace_eq_top [IsAlgClosed K] [FiniteDimensional K V] (f -- We prove the claim by strong induction on the dimension of the vector space. suffices ∀ n, finrank K V = n → ⨆ (μ : K), f.maxGenEigenspace μ = ⊤ by exact this _ rfl intro n h_dim - induction n using Nat.strong_induction_on generalizing V with | h n ih => + induction n using Nat.strong_induction_on generalizing V with | ind n ih rcases n with - | n -- If the vector space is 0-dimensional, the result is trivial. · rw [← top_le_iff] diff --git a/Mathlib/LinearAlgebra/Finsupp/Pi.lean b/Mathlib/LinearAlgebra/Finsupp/Pi.lean index b182855f479a7b..62c4950ee62798 100644 --- a/Mathlib/LinearAlgebra/Finsupp/Pi.lean +++ b/Mathlib/LinearAlgebra/Finsupp/Pi.lean @@ -138,7 +138,7 @@ theorem prodOfFinsuppNat_injective (inj : Injective f) : Injective (prodOfFinsup · simp_all [s] set n := s.max' ne with hn clear_value n; revert x y - induction n using Nat.strong_induction_on with | h n ih => + induction n using Nat.strong_induction_on with | ind n ih intro x y s _ hn eq rw [← x.single_add_erase 0, ← y.single_add_erase 0] simp_rw [← mapDomain_comapDomain_nat_add_one, ← f.fst_prodOfFinsuppNat, eq] diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean index 6c744b0fe0734a..0aae707f986d79 100644 --- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean +++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean @@ -487,7 +487,7 @@ coordinate. Here, we give an auxiliary statement tailored for an inductive proof theorem map_sum_finset_aux [DecidableEq ι] [Fintype ι] {n : ℕ} (h : (∑ i, #(A i)) = n) : (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i) := by letI := fun i => Classical.decEq (α i) - induction n using Nat.strong_induction_on generalizing A with | h n IH => + induction n using Nat.strong_induction_on generalizing A with | ind n IH -- If one of the sets is empty, then all the sums are zero by_cases! Ai_empty : ∃ i, A i = ∅ · obtain ⟨i, hi⟩ : ∃ i, ∑ j ∈ A i, g i j = 0 := Ai_empty.imp fun i hi ↦ by simp [hi] diff --git a/Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean b/Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean index 3cceccbb2e484a..472f063f297419 100644 --- a/Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean +++ b/Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Defs.lean @@ -338,7 +338,7 @@ lemma IsLinearSet.isProperSemilinearSet [IsCancelAdd M] (hs : IsLinearSet s) : classical rw [isLinearSet_iff] at hs rcases hs with ⟨a, t, rfl⟩ - induction hn : t.card using Nat.strong_induction_on generalizing a t with | _ n ih + induction hn : t.card using Nat.strong_induction_on generalizing a t with | ind n ih subst hn by_cases hindep : LinearIndepOn ℕ id (t : Set M) · exact IsProperLinearSet.isProperSemilinearSet ⟨a, t, by simpa⟩ @@ -353,7 +353,7 @@ lemma IsLinearSet.isProperSemilinearSet [IsCancelAdd M] (hs : IsLinearSet s) : · rintro ⟨y, hy, rfl⟩ rw [mem_closure_finset] at hy rcases hy with ⟨g, -, rfl⟩ - induction hn : g i using Nat.strong_induction_on generalizing g with | _ n ih' + induction hn : g i using Nat.strong_induction_on generalizing g with | ind n ih' subst hn by_cases! hfg : ∀ j ∈ t', f j ≤ g j · convert! diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean index 9a289e32988008..36e175fc87ff40 100644 --- a/Mathlib/NumberTheory/Bernoulli.lean +++ b/Mathlib/NumberTheory/Bernoulli.lean @@ -643,7 +643,7 @@ private lemma bernoulli_add_indicator_eq_sub {k p : ℕ} (hk : k > 0) [Fact p.Pr private lemma not_dvd_den_bernoulli_add_indicator {k p : ℕ} (hk : k > 0) [Fact p.Prime] : ¬ p ∣ (bernoulli (2 * k) + vonStaudtIndicator (2 * k) p / p).den := by induction k using Nat.strong_induction_on with - | _ k ih => + | ind k ih => obtain ⟨T, hT⟩ := bernoulli_add_indicator_eq_sub (p := p) hk rw [hT] have hT_int : pIntegral p T := Int.padicValuation_le_one p T diff --git a/Mathlib/NumberTheory/BernoulliPolynomials.lean b/Mathlib/NumberTheory/BernoulliPolynomials.lean index 21a770d7a26655..cdfcc51bdc44b4 100644 --- a/Mathlib/NumberTheory/BernoulliPolynomials.lean +++ b/Mathlib/NumberTheory/BernoulliPolynomials.lean @@ -182,7 +182,7 @@ theorem bernoulli_succ_eval (n p : ℕ) : (bernoulli p.succ).eval (n : ℚ) = set_option backward.isDefEq.respectTransparency false in theorem bernoulli_comp_one_add_X (n : ℕ) : (bernoulli n).comp (1 + X) = bernoulli n + n • X ^ (n - 1) := by - refine Nat.strong_induction_on n fun d hd => ?_ + induction n using Nat.strong_induction_on with | ind d hd cases d with | zero => simp | succ d => diff --git a/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean b/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean index 704a720427df65..2c652dbf9619be 100644 --- a/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean +++ b/Mathlib/NumberTheory/DiophantineApproximation/Basic.lean @@ -491,7 +491,7 @@ end /-- The technical version of *Legendre's Theorem*. -/ theorem exists_rat_eq_convergent' {v : ℕ} (h : ContfracLegendre.Ass ξ u v) : ∃ n, (u / v : ℚ) = ξ.convergent n := by - induction v using Nat.strong_induction_on generalizing ξ u with | h v ih => ?_ + induction v using Nat.strong_induction_on generalizing ξ u with | ind v ih rcases lt_trichotomy v 1 with (ht | rfl | ht) · replace h := h.2.2 simp only [Nat.lt_one_iff.mp ht, Nat.cast_zero, div_zero, tsub_zero, zero_mul, diff --git a/Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean b/Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean index 338c97bf8495d0..9ad9d1e23ae6da 100644 --- a/Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean +++ b/Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean @@ -248,7 +248,7 @@ theorem levelOne_weight_two_rank_zero : Module.rank ℂ (ModularForm 𝒮ℒ 2) theorem dimension_level_one (k : ℕ) (hk2 : Even k) : Module.rank ℂ (ModularForm 𝒮ℒ k) = if k ≡ 2 [MOD 12] then k / 12 else k / 12 + 1 := by - induction k using Nat.strong_induction_on with | h k ihn => + induction k using Nat.strong_induction_on with | ind k ihn have : k < 3 ∨ (3 ≤ k ∧ k < 12) ∨ 12 ≤ k := by grind rcases this with hk | hk | hk · -- `k < 3`: direct case-by-case check @@ -285,7 +285,7 @@ instance (k : ℤ) : FiniteDimensional ℂ (ModularForm 𝒮ℒ k) := by `k : ℕ` has q-expansion of order strictly greater than `k / 12`, then `f` is identically zero. -/ theorem sturm_bound_levelOne_nat {k : ℕ} {f : ModularForm 𝒮ℒ (k : ℤ)} (h : (↑(k / 12) : ℕ∞) < (qExpansion 1 f).order) : f = 0 := by - induction k using Nat.strong_induction_on with | _ k ih => + induction k using Nat.strong_induction_on with | ind k ih have h0 : (qExpansion 1 f).coeff 0 = 0 := PowerSeries.coeff_of_lt_order _ ((Nat.cast_nonneg _).trans_lt h) suffices CuspForm.discriminantEquiv (toCuspForm f h0) = 0 by diff --git a/Mathlib/NumberTheory/Pell.lean b/Mathlib/NumberTheory/Pell.lean index 8b68eb9388aeb0..f6e12b7e4175c1 100644 --- a/Mathlib/NumberTheory/Pell.lean +++ b/Mathlib/NumberTheory/Pell.lean @@ -590,7 +590,7 @@ theorem mul_inv_x_lt_x {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solu theorem eq_pow_of_nonneg {a₁ : Solution₁ d} (h : IsFundamental a₁) {a : Solution₁ d} (hax : 0 < a.x) (hay : 0 ≤ a.y) : ∃ n : ℕ, a = a₁ ^ n := by lift a.x to ℕ using hax.le with ax hax' - induction ax using Nat.strong_induction_on generalizing a with | h x ih => + induction ax using Nat.strong_induction_on generalizing a with | ind x ih rcases hay.eq_or_lt with hy | hy · -- case 1: `a = 1` refine ⟨0, ?_⟩ diff --git a/Mathlib/NumberTheory/Primorial.lean b/Mathlib/NumberTheory/Primorial.lean index 147e83d499d4d4..6a6210453a914f 100644 --- a/Mathlib/NumberTheory/Primorial.lean +++ b/Mathlib/NumberTheory/Primorial.lean @@ -120,7 +120,7 @@ lemma le_primorial_self {n : ℕ} : n ≤ n# := by · exact (lt_primorial_self hn).le theorem primorial_lt_four_pow (n : ℕ) (hn : n ≠ 0) : n# < 4 ^ n := by - induction n using Nat.strong_induction_on with | h n ihn => + induction n using Nat.strong_induction_on with | ind n ihn rcases n with - | n; · grind rcases n.even_or_odd with ⟨m, rfl⟩ | ho · rcases m.eq_zero_or_pos with rfl | hm diff --git a/Mathlib/Order/Fin/Basic.lean b/Mathlib/Order/Fin/Basic.lean index 84f14489c0d9eb..a8d717b53e1dbe 100644 --- a/Mathlib/Order/Fin/Basic.lean +++ b/Mathlib/Order/Fin/Basic.lean @@ -396,7 +396,7 @@ map. In this lemma we state that for each `i : Fin n` we have `(e i : ℕ) = (i @[simp] lemma coe_orderIso_apply (e : Fin n ≃o Fin m) (i : Fin n) : (e i : ℕ) = i := by rcases i with ⟨i, hi⟩ dsimp only - induction i using Nat.strong_induction_on with | _ i h + induction i using Nat.strong_induction_on with | ind i h refine le_antisymm (forall_lt_iff_le.1 fun j hj => ?_) (forall_lt_iff_le.1 fun j hj => ?_) · have := e.symm.lt_symm_apply.1 (mk_lt_of_lt_val hj) specialize h _ this (e.symm _).is_lt diff --git a/Mathlib/Order/KrullDimension.lean b/Mathlib/Order/KrullDimension.lean index b40d78664694ba..c94a44aaa24b83 100644 --- a/Mathlib/Order/KrullDimension.lean +++ b/Mathlib/Order/KrullDimension.lean @@ -1105,7 +1105,7 @@ lemma height_le_of_krullDim_preimage_le (x : α) : Order.height x ≤ (m + 1) * Order.height (f x) + m := by generalize h' : Order.height (f x) = n cases n with | top => simp | coe n => - induction n using Nat.strong_induction_on generalizing x with | h n ih => + induction n using Nat.strong_induction_on generalizing x with | ind n ih refine height_le_iff.mpr fun p hp ↦ le_of_not_gt fun h_len ↦ ?_ let i : Fin (p.length + 1) := ⟨p.length - (m + 1), Nat.sub_lt_succ p.length _⟩ suffices h'' : f (p i) < f x by diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean index bf58bd9bd4f793..4f16c220d95e56 100644 --- a/Mathlib/RingTheory/AdjoinRoot.lean +++ b/Mathlib/RingTheory/AdjoinRoot.lean @@ -1080,7 +1080,7 @@ lemma Polynomial.Monic.exists_splits_map.{u} {R : Type u} [CommRing R] [Nontrivial R] {p : R[X]} (hp : p.Monic) : ∃ (S : Type u) (_ : CommRing S) (_ : Algebra R S) (_ : Module.Finite R S) (_ : Module.Free R S) (_ : Nontrivial S), (p.map (algebraMap R S)).Splits := by - induction hn : p.natDegree using Nat.strong_induction_on generalizing R with | h n IH => + induction hn : p.natDegree using Nat.strong_induction_on generalizing R with | ind n IH by_cases hpu : IsUnit p · obtain rfl := hp.eq_one_of_isUnit hpu exact ⟨R, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance, by simp⟩ diff --git a/Mathlib/RingTheory/Etale/QuasiFinite.lean b/Mathlib/RingTheory/Etale/QuasiFinite.lean index cfeb0d8b82fcf4..7bf063474af4c2 100644 --- a/Mathlib/RingTheory/Etale/QuasiFinite.lean +++ b/Mathlib/RingTheory/Etale/QuasiFinite.lean @@ -530,7 +530,7 @@ private lemma Algebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver ∀ (P'' : Ideal (R' ⊗[R] S)), P''.IsPrime → P''.LiesOver P → e (.last n) ∈ P'' ∧ ∀ i, e i.castSucc ∉ P'' → P'' = P' i := by induction h : (p.primesOver S).ncard using Nat.strong_induction_on generalizing R S with - | h n IH => + | ind n IH => have : IsArtinianRing (p.ResidueField ⊗[R] S) := IsArtinianRing.of_finite p.ResidueField _ have hpSfin : (p.primesOver S).Finite := (PrimeSpectrum.primesOverOrderIsoFiber R S p).finite_iff.mpr inferInstance diff --git a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean index beef0a92dab0c1..284f648ee878e4 100644 --- a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean +++ b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean @@ -188,7 +188,7 @@ nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff] rintro ⟨s, (rfl : span s = I)⟩ induction hn : s.card using Nat.strong_induction_on generalizing R with - | h n H => + | ind n H => replace hn : s.card ≤ n := hn.le have := hp.isPrime cases n with diff --git a/Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean b/Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean index 1776fae04849ee..e9c532436aeee4 100644 --- a/Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean +++ b/Mathlib/RingTheory/Ideal/Quotient/Nilpotent.lean @@ -30,7 +30,7 @@ theorem Ideal.IsNilpotent.induction_on (hI : IsNilpotent I) P (J.map (Ideal.Quotient.mk I)) → P J) : P I := by obtain ⟨n, hI : I ^ n = ⊥⟩ := hI - induction n using Nat.strong_induction_on generalizing S with | _ n H + induction n using Nat.strong_induction_on generalizing S with | ind n H by_cases hI' : I = ⊥ · subst hI' apply h₁ diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean index 91031e26fe3cd9..7367aeabfaaaf4 100644 --- a/Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean +++ b/Mathlib/RingTheory/IntegralClosure/IsIntegral/AlmostIntegral.lean @@ -56,7 +56,7 @@ lemma IsIntegral.isAlmostIntegral_of_exists_smul_mem_range rw [← Nat.sub_add_cancel hi.le, pow_add, mul_smul, ← smul_pow] exact (AlgHom.range (Algebra.ofId _ _)).smul_mem (Subalgebra.pow_mem _ ht' _) _ refine ⟨b, hb', fun n ↦ ?_⟩ - induction n using Nat.strong_induction_on with | h n IH => + induction n using Nat.strong_induction_on with | ind n IH obtain hn | hn := lt_or_ge n (minpoly R s).natDegree · exact hb _ (by simpa) have := minpoly.aeval R s diff --git a/Mathlib/RingTheory/LittleWedderburn.lean b/Mathlib/RingTheory/LittleWedderburn.lean index 20425e0914f877..aa9aeeb6544f31 100644 --- a/Mathlib/RingTheory/LittleWedderburn.lean +++ b/Mathlib/RingTheory/LittleWedderburn.lean @@ -143,7 +143,7 @@ end InductionHyp private theorem center_eq_top [Finite D] : Subring.center D = ⊤ := by classical cases nonempty_fintype D - induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | _ n IH + induction hn : Fintype.card D using Nat.strong_induction_on generalizing D with | ind n IH apply InductionHyp.center_eq_top intro R hR x y hx hy suffices (⟨y, hy⟩ : R) ∈ Subring.center R by diff --git a/Mathlib/RingTheory/Polynomial/Basic.lean b/Mathlib/RingTheory/Polynomial/Basic.lean index bc3e957ea17a99..7f9ea7946837a3 100644 --- a/Mathlib/RingTheory/Polynomial/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Basic.lean @@ -648,7 +648,7 @@ theorem is_fg_degreeLE [IsNoetherianRing R] (I : Ideal R[X]) (n : ℕ) : lemma map_C_comap_of_comap_eq_leadingCoeff (I : Ideal R[X]) (hI : comap C I = I.leadingCoeff) : map C (comap C I) = I := by refine le_antisymm map_comap_le (fun f hfI ↦ ?_) - induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | _ _ ih + induction hn : f.natDegree using Nat.strong_induction_on generalizing f with | ind _ ih have h : C f.leadingCoeff * X ^ f.natDegree ∈ map C (comap C I) := (map C (comap C I)).mul_mem_right (X ^ f.natDegree) <| mem_map_of_mem C <| by simpa [hI] using (I.mem_leadingCoeff f.leadingCoeff).2 ⟨f, hfI, rfl⟩ @@ -799,7 +799,7 @@ protected theorem Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNo rw [this] intro p hp generalize hn : p.natDegree = k - induction k using Nat.strong_induction_on generalizing p with | _ k ih + induction k using Nat.strong_induction_on generalizing p with | ind k ih rcases le_or_gt k N with h | h · subst k refine hs2 ⟨Polynomial.mem_degreeLE.2 diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean index 05e37ed8dd0363..52dd9c388e03dd 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean @@ -180,7 +180,7 @@ theorem int_coeff_of_cyclotomic' {K : Type*} [CommRing K] [IsDomain K] {ζ : K} (h : IsPrimitiveRoot ζ n) : ∃ P : ℤ[X], map (Int.castRingHom K) P = cyclotomic' n K ∧ P.degree = (cyclotomic' n K).degree ∧ P.Monic := by refine lifts_and_degree_eq_and_monic ?_ (cyclotomic'.monic n K) - induction n using Nat.strong_induction_on generalizing ζ with | _ k ihk + induction n using Nat.strong_induction_on generalizing ζ with | ind k ihk rcases k.eq_zero_or_pos with (rfl | hpos) · use 1 simp only [cyclotomic'_zero, coe_mapRingHom, Polynomial.map_one] @@ -476,7 +476,7 @@ theorem X_pow_sub_one_dvd_prod_cyclotomic (R : Type*) [CommRing R] {n m : ℕ} ( theorem cyclotomic_eq_prod_X_sub_primitiveRoots {K : Type*} [CommRing K] [IsDomain K] {ζ : K} {n : ℕ} (hz : IsPrimitiveRoot ζ n) : cyclotomic n K = ∏ μ ∈ primitiveRoots n K, (X - C μ) := by rw [← cyclotomic'] - induction n using Nat.strong_induction_on generalizing ζ with | _ k hk + induction n using Nat.strong_induction_on generalizing ζ with | ind k hk obtain hzero | hpos := k.eq_zero_or_pos · simp only [hzero, cyclotomic'_zero, cyclotomic_zero] have h : ∀ i ∈ k.properDivisors, cyclotomic i K = cyclotomic' i K := by @@ -533,7 +533,7 @@ theorem cyclotomic_prime_pow_mul_X_pow_sub_one (R : Type*) [CommRing R] (p k : /-- The constant term of `cyclotomic n R` is `1` if `2 ≤ n`. -/ theorem cyclotomic_coeff_zero (R : Type*) [CommRing R] {n : ℕ} (hn : 1 < n) : (cyclotomic n R).coeff 0 = 1 := by - induction n using Nat.strong_induction_on with | _ n hi + induction n using Nat.strong_induction_on with | ind n hi have hprod : (∏ i ∈ Nat.properDivisors n, (Polynomial.cyclotomic i R).coeff 0) = -1 := by rw [← Finset.insert_erase (Nat.one_mem_properDivisors_iff_one_lt.2 (lt_of_lt_of_le one_lt_two hn)), Finset.prod_insert (Finset.notMem_erase 1 _), diff --git a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean index eb538bb3c80dae..ea315741242231 100644 --- a/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean +++ b/Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean @@ -69,7 +69,7 @@ private theorem cyclotomic_neg_one_pos {n : ℕ} (hn : 2 < n) {R} theorem cyclotomic_pos {n : ℕ} (hn : 2 < n) {R} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (x : R) : 0 < eval x (cyclotomic n R) := by - induction n using Nat.strong_induction_on with | _ n ih + induction n using Nat.strong_induction_on with | ind n ih have hn' : 0 < n := pos_of_gt hn have hn'' : 1 < n := one_lt_two.trans hn have := prod_cyclotomic_eq_geom_sum hn' R diff --git a/Mathlib/RingTheory/Polynomial/IsIntegral.lean b/Mathlib/RingTheory/Polynomial/IsIntegral.lean index 1bda775fc4645b..74f2d1d4a0a9c7 100644 --- a/Mathlib/RingTheory/Polynomial/IsIntegral.lean +++ b/Mathlib/RingTheory/Polynomial/IsIntegral.lean @@ -97,7 +97,7 @@ lemma IsAlmostIntegral.coeff [IsDomain R] [FaithfulSMul R S] simp only [← leadingCoeff_map_of_injective (FaithfulSMul.algebraMap_injective R S), hr] at h ⊢ rw [← leadingCoeff_pow' h'] at h ⊢ rw [leadingCoeff_mul' h] - induction hn : p.natDegree using Nat.strong_induction_on generalizing p with | h n IH => + induction hn : p.natDegree using Nat.strong_induction_on generalizing p with | ind n IH by_cases hp' : p.natDegree = 0 · obtain ⟨p, rfl⟩ := natDegree_eq_zero.mp hp' simp only [coeff_C] diff --git a/Mathlib/RingTheory/Polynomial/Nilpotent.lean b/Mathlib/RingTheory/Polynomial/Nilpotent.lean index 83a2a569d2e3b5..e9dac8794ef384 100644 --- a/Mathlib/RingTheory/Polynomial/Nilpotent.lean +++ b/Mathlib/RingTheory/Polynomial/Nilpotent.lean @@ -110,7 +110,7 @@ nilpotent, then `P` is a unit. See also `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent`. -/ theorem isUnit_of_coeff_isUnit_isNilpotent (hunit : IsUnit (P.coeff 0)) (hnil : ∀ i, i ≠ 0 → IsNilpotent (P.coeff i)) : IsUnit P := by - induction h : P.natDegree using Nat.strong_induction_on generalizing P with | _ k hind + induction h : P.natDegree using Nat.strong_induction_on generalizing P with | ind k hind by_cases hdeg : P.natDegree = 0 · rw [eq_C_of_natDegree_eq_zero hdeg] exact hunit.map C diff --git a/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean b/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean index 8ca60864c4d48a..f19e68650d3a85 100644 --- a/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean +++ b/Mathlib/RingTheory/Polynomial/Resultant/Basic.lean @@ -414,7 +414,7 @@ lemma resultant_eq_prod_roots_sub simp [hf'.natDegree_eq_card_roots, hg'.natDegree_eq_card_roots] · simp generalize hN : f.natDegree + g.natDegree = N - induction N using Nat.strong_induction_on generalizing K with | h n IH => + induction N using Nat.strong_induction_on generalizing K with | ind n IH by_cases hr : g ∣ f · obtain ⟨r, rfl⟩ := hr have hr' : r ≠ 0 := by simpa [hg.ne_zero] using hf.ne_zero diff --git a/Mathlib/RingTheory/WittVector/Defs.lean b/Mathlib/RingTheory/WittVector/Defs.lean index 7f61d1db574cc9..b9ec0da909b539 100644 --- a/Mathlib/RingTheory/WittVector/Defs.lean +++ b/Mathlib/RingTheory/WittVector/Defs.lean @@ -222,7 +222,7 @@ theorem wittOne_zero_eq_one : wittOne p 0 = 1 := by theorem wittOne_pos_eq_zero (n : ℕ) (hn : 0 < n) : wittOne p n = 0 := by apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective simp only [wittOne, wittStructureRat, map_zero, map_one, map_wittStructureInt] - induction n using Nat.strong_induction_on with | h n IH => ?_ + induction n using Nat.strong_induction_on with | ind n IH rw [xInTermsOfW_eq] simp only [map_mul, map_sub, map_sum, map_pow, bind₁_X_right, bind₁_C_right] diff --git a/Mathlib/RingTheory/WittVector/Frobenius.lean b/Mathlib/RingTheory/WittVector/Frobenius.lean index 83e2d0296f451b..7129a3d9da47c3 100644 --- a/Mathlib/RingTheory/WittVector/Frobenius.lean +++ b/Mathlib/RingTheory/WittVector/Frobenius.lean @@ -134,8 +134,7 @@ theorem map_frobeniusPoly (n : ℕ) : MvPolynomial.map (Int.castRingHom ℚ) (frobeniusPoly p n) = frobeniusPolyRat p n := by rw [frobeniusPoly, map_add, map_mul, map_pow, map_C, map_X, eq_intCast, Int.cast_natCast, frobeniusPolyRat] - refine Nat.strong_induction_on n ?_; clear n - intro n IH + induction n using Nat.strong_induction_on n with | ind n IH rw [xInTermsOfW_eq] simp only [map_sum, map_sub, map_mul, map_pow (bind₁ _), bind₁_C_right] have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow] diff --git a/Mathlib/RingTheory/WittVector/StructurePolynomial.lean b/Mathlib/RingTheory/WittVector/StructurePolynomial.lean index cc98c44df9f9a9..42308278e8faa4 100644 --- a/Mathlib/RingTheory/WittVector/StructurePolynomial.lean +++ b/Mathlib/RingTheory/WittVector/StructurePolynomial.lean @@ -266,7 +266,7 @@ variable (p) theorem map_wittStructureInt (Φ : MvPolynomial idx ℤ) (n : ℕ) : map (Int.castRingHom ℚ) (wittStructureInt p Φ n) = wittStructureRat p (map (Int.castRingHom ℚ) Φ) n := by - induction n using Nat.strong_induction_on with | h n IH => ?_ + induction n using Nat.strong_induction_on with | ind n IH rw [wittStructureInt, map_mapRange_eq_iff, Int.coe_castRingHom] intro c rw [wittStructureRat_rec, coeff_C_mul, mul_comm, mul_div_assoc', mul_one] diff --git a/Mathlib/RingTheory/ZariskisMainTheorem.lean b/Mathlib/RingTheory/ZariskisMainTheorem.lean index 1d7ad580fa7bd8..59169fab5d43cd 100644 --- a/Mathlib/RingTheory/ZariskisMainTheorem.lean +++ b/Mathlib/RingTheory/ZariskisMainTheorem.lean @@ -264,8 +264,7 @@ lemma exists_leadingCoeff_pow_smul_mem_radical_conductor wlog hi : i = p.natDegree generalizing p i · clear hi simp only [forall_eq, coeff_natDegree] at this - induction hpn : p.natDegree using Nat.strong_induction_on generalizing p with - | h n IH => + induction hpn : p.natDegree using Nat.strong_induction_on generalizing p with | ind n IH cases n with | zero => obtain hi' | hi' := lt_or_ge p.natDegree i @@ -480,7 +479,7 @@ private lemma ZariskisMainProperty.of_adjoin_eq_top (Polynomial.not_ker_le_map_C_of_surjective_of_weaklyQuasiFiniteAt _ H₀ p) obtain ⟨n, hfn⟩ : ∃ x, algebraMap R S (f.coeff x) ∉ p := by simpa [Ideal.mem_map_C_iff] using! hfp clear hfp - induction hm : f.natDegree using Nat.strong_induction_on generalizing f n with | h m IH => + induction hm : f.natDegree using Nat.strong_induction_on generalizing f n with | ind m IH obtain (_ | m) := m · obtain ⟨r, rfl⟩ := natDegree_eq_zero.mp hm cases n <;> aesop diff --git a/Mathlib/Topology/Metrizable/Uniformity.lean b/Mathlib/Topology/Metrizable/Uniformity.lean index 65a49d6ea9e06f..33c47ac1fcac82 100644 --- a/Mathlib/Topology/Metrizable/Uniformity.lean +++ b/Mathlib/Topology/Metrizable/Uniformity.lean @@ -120,7 +120,7 @@ theorem le_two_mul_dist_ofPreNNDist (d : X → X → ℝ≥0) (dist_self : ∀ x simpa only [nonpos_iff_eq_zero, hab, hbc, dist_self c, max_self, mul_zero] using hd a b c c suffices ∀ n, length l = n → d x y ≤ 2 * (zipWith d (x :: l) (l ++ [y])).sum by exact this _ rfl intro n hn - induction n using Nat.strong_induction_on generalizing x y l with | h n ihn => + induction n using Nat.strong_induction_on generalizing x y l with | ind n ihn subst n set L := zipWith d (x::l) (l ++ [y]) have hL_len : length L = length l + 1 := by simp [L] From 99c4a399b8dbb4c38ec378bb2c91cc0c190366f7 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Thu, 9 Jul 2026 13:03:17 -0400 Subject: [PATCH 2/3] fix fix --- Mathlib/Data/Fin/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean index 3456d45fc4e203..2d9ff2ec90e51b 100644 --- a/Mathlib/Data/Fin/Basic.lean +++ b/Mathlib/Data/Fin/Basic.lean @@ -466,7 +466,7 @@ lemma strong_induction_on {n : ℕ} {motive : Fin n → Prop} motive i := by obtain ⟨i, hi⟩ := i induction i using Nat.strong_induction_on with - | ind j hj => exact h _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁) + | ind j hj => exact ind _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁) end Rec From b0b6ea8060d74df1579585a205770a7557a6cd83 Mon Sep 17 00:00:00 2001 From: Aaron Liu Date: Thu, 9 Jul 2026 14:29:17 -0400 Subject: [PATCH 3/3] fix fix 2 --- Mathlib/Algebra/Lie/LieTheorem.lean | 2 +- Mathlib/RingTheory/WittVector/Frobenius.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Lie/LieTheorem.lean b/Mathlib/Algebra/Lie/LieTheorem.lean index 7d83f6ca7eeb1e..c521314cc8e383 100644 --- a/Mathlib/Algebra/Lie/LieTheorem.lean +++ b/Mathlib/Algebra/Lie/LieTheorem.lean @@ -126,7 +126,7 @@ private lemma weightSpaceOfIsLieTower_aux (z : L) (v : V) (hv : v ∈ weightSpac apply iSup_le intro i x hx simp only [Module.End.mem_maxGenEigenspace, zero_smul, sub_zero] - induction i using Nat.strong_induction_on generalizing x | ind i ih + induction i using Nat.strong_induction_on generalizing x with | ind i ih obtain rfl | hi := eq_or_ne i 0 · simp_all [U'] obtain ⟨j, hj, hj'⟩ := key i hi diff --git a/Mathlib/RingTheory/WittVector/Frobenius.lean b/Mathlib/RingTheory/WittVector/Frobenius.lean index 7129a3d9da47c3..7a5c65ff2648e2 100644 --- a/Mathlib/RingTheory/WittVector/Frobenius.lean +++ b/Mathlib/RingTheory/WittVector/Frobenius.lean @@ -134,7 +134,7 @@ theorem map_frobeniusPoly (n : ℕ) : MvPolynomial.map (Int.castRingHom ℚ) (frobeniusPoly p n) = frobeniusPolyRat p n := by rw [frobeniusPoly, map_add, map_mul, map_pow, map_C, map_X, eq_intCast, Int.cast_natCast, frobeniusPolyRat] - induction n using Nat.strong_induction_on n with | ind n IH + induction n using Nat.strong_induction_on with | ind n IH rw [xInTermsOfW_eq] simp only [map_sum, map_sub, map_mul, map_pow (bind₁ _), bind₁_C_right] have h1 : (p : ℚ) ^ n * ⅟(p : ℚ) ^ n = 1 := by rw [← mul_pow, mul_invOf_self, one_pow]