chore: rename arguments of Nat.strong_induction_on

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

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

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 with | ind i ih
     obtain rfl | hi := eq_or_ne i 0
     · simp_all [U']
     obtain ⟨j, hj, hj'⟩ := key i hi

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]

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])

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

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]

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 => ?_

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)

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

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}

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

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 ind _ (fun ⟨k, hk₁⟩ hk₂ ↦ hj _ hk₂ hk₁)
 
 end Rec
 

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

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

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]

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]

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 :=

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

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⟩

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]

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

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'⟩

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]

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]

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]

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!

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

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 =>

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,

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

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, ?_⟩

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

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

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