chore: deprime induction in Archive and SetTheory (leanprover-community#25512)

I have decided that depriming one folder (or part of a folder) at a time is the way to go.

Author: Parcly-Taxel

Archive/Imo/Imo1977Q6.lean

@@ -19,11 +19,10 @@ then we use it to prove the statement for positive naturals.
 namespace Imo1977Q6
 
 theorem imo1977_q6_nat (f : ℕ → ℕ) (h : ∀ n, f (f n) < f (n + 1)) : ∀ n, f n = n := by
-  have h' : ∀ k n : ℕ, k ≤ n → k ≤ f n := by
-    intro k
-    induction' k with k h_ind
-    · intros; exact Nat.zero_le _
-    · intro n hk
+  have h' (k n : ℕ) (hk : k ≤ n) : k ≤ f n := by
+    induction k generalizing n with
+    | zero => exact Nat.zero_le _
+    | succ k h_ind =>
       apply Nat.succ_le_of_lt
       calc
         k ≤ f (f (n - 1)) := h_ind _ (h_ind (n - 1) (le_tsub_of_add_le_right hk))

Archive/Imo/Imo2006Q5.lean

@@ -89,11 +89,11 @@ theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
           (fun x => P.eval x)^[n + 1] t - (fun x => P.eval x)^[n] t :=
       fun m n => Cycle.chain_iff_pairwise.1 HC' _ HC _ HC
     -- The sign of P^n(t) - t is the same as P(t) - t for positive n. Proven by induction on n.
-    have IH : ∀ n : ℕ, ((fun x => P.eval x)^[n + 1] t - t).sign = (P.eval t - t).sign := by
-      intro n
-      induction' n with n IH
-      · rfl
-      · apply Eq.trans _ (Int.sign_add_eq_of_sign_eq IH)
+    have IH (n : ℕ) : ((fun x => P.eval x)^[n + 1] t - t).sign = (P.eval t - t).sign := by
+      induction n with
+      | zero => rfl
+      | succ n IH =>
+        apply Eq.trans _ (Int.sign_add_eq_of_sign_eq IH)
         have H := Heq n.succ 0
         dsimp at H ⊢
         rw [← H, sub_add_sub_cancel']

Archive/Imo/Imo2013Q1.lean

@@ -43,9 +43,9 @@ open Imo2013Q1
 theorem imo2013_q1 (n : ℕ+) (k : ℕ) :
     ∃ m : ℕ → ℕ+, (1 : ℚ) + (2 ^ k - 1) / n = ∏ i ∈ Finset.range k, (1 + 1 / (m i : ℚ)) := by
   revert n
-  induction' k with pk hpk
-  · intro n; use fun (_ : ℕ) => (1 : ℕ+); simp
-  -- For the base case, any m works.
+  induction k with
+  | zero => intro n; use fun (_ : ℕ) => (1 : ℕ+); simp -- For the base case, any m works.
+  | succ pk hpk =>
   intro n
   obtain ⟨t, ht : ↑n = t + t⟩ | ⟨t, ht : ↑n = 2 * t + 1⟩ := (n : ℕ).even_or_odd
   · -- even case

Archive/Imo/Imo2013Q5.lean

@@ -113,16 +113,17 @@ theorem fx_gt_xm1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 ≤ x)
 theorem pow_f_le_f_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n) {x : ℚ} (hx : 1 < x)
     (H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y) (H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n) :
     f (x ^ n) ≤ f x ^ n := by
-  induction' n with pn hpn
-  · exfalso; exact Nat.lt_asymm hn hn
-  rcases pn with - | pn
-  · norm_num
-  have hpn' := hpn pn.succ_pos
-  rw [pow_succ x (pn + 1), pow_succ (f x) (pn + 1)]
-  have hxp : 0 < x := by positivity
-  calc
-    f (x ^ (pn + 1) * x) ≤ f (x ^ (pn + 1)) * f x := H1 (x ^ (pn + 1)) x (pow_pos hxp (pn + 1)) hxp
-    _ ≤ f x ^ (pn + 1) * f x := by gcongr; exact (f_pos_of_pos hxp H1 H4).le
+  induction n with
+  | zero => exfalso; exact Nat.lt_asymm hn hn
+  | succ pn hpn =>
+    rcases pn with - | pn
+    · norm_num
+    have hpn' := hpn pn.succ_pos
+    rw [pow_succ x (pn + 1), pow_succ (f x) (pn + 1)]
+    have hxp : 0 < x := by positivity
+    calc
+      _ ≤ f (x ^ (pn + 1)) * f x := H1 (x ^ (pn + 1)) x (pow_pos hxp (pn + 1)) hxp
+      _ ≤ f x ^ (pn + 1) * f x := by gcongr; exact (f_pos_of_pos hxp H1 H4).le
 
 theorem fixed_point_of_pos_nat_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n)
     (H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y) (H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n)
@@ -169,15 +170,16 @@ theorem imo2013_q5 (f : ℚ → ℝ) (H1 : ∀ x y, 0 < x → 0 < y → f (x * y
     intro x hx n hn
     rcases n with - | n
     · exact (lt_irrefl 0 hn).elim
-    induction' n with pn hpn
-    · norm_num
-    calc
-      ↑(pn + 2) * f x = (↑pn + 1 + 1) * f x := by norm_cast
-      _ = (↑pn + 1) * f x + f x := by ring
-      _ ≤ f (↑pn.succ * x) + f x := mod_cast add_le_add_right (hpn pn.succ_pos) (f x)
-      _ ≤ f ((↑pn + 1) * x + x) := by exact_mod_cast H2 _ _ (mul_pos pn.cast_add_one_pos hx) hx
-      _ = f ((↑pn + 1 + 1) * x) := by ring_nf
-      _ = f (↑(pn + 2) * x) := by norm_cast
+    induction n with
+    | zero => norm_num
+    | succ pn hpn =>
+      calc
+        ↑(pn + 2) * f x = (↑pn + 1 + 1) * f x := by norm_cast
+        _ = (↑pn + 1) * f x + f x := by ring
+        _ ≤ f (↑pn.succ * x) + f x := mod_cast add_le_add_right (hpn pn.succ_pos) (f x)
+        _ ≤ f ((↑pn + 1) * x + x) := by exact_mod_cast H2 _ _ (mul_pos pn.cast_add_one_pos hx) hx
+        _ = f ((↑pn + 1 + 1) * x) := by ring_nf
+        _ = f (↑(pn + 2) * x) := by norm_cast
   have H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n := by
     intro n hn
     have hf1 : 1 ≤ f 1 := by

Archive/Imo/Imo2019Q1.lean

@@ -39,10 +39,11 @@ theorem imo2019_q1 (f : ℤ → ℤ) :
   -- Hence, `f` is an affine map, `f b = f 0 + m * b`
   obtain ⟨c, H⟩ : ∃ c, ∀ b, f b = c + m * b := by
     refine ⟨f 0, fun b => ?_⟩
-    induction' b with b ihb b ihb
-    · simp
-    · simp [H, ihb, mul_add, add_assoc]
-    · rw [← sub_eq_of_eq_add (H _)]
+    induction b with
+    | zero => simp
+    | succ b ihb => simp [H, ihb, mul_add, add_assoc]
+    | pred b ihb =>
+      rw [← sub_eq_of_eq_add (H _)]
       simp [ihb]; ring
   -- Now use `hf 0 0` and `hf 0 1` to show that `m ∈ {0, 2}`
   have H3 : 2 * c = m * c := by simpa [H, mul_add] using hf 0 0

Archive/Imo/Imo2019Q4.lean

@@ -61,20 +61,21 @@ theorem upper_bound {k n : ℕ} (hk : k > 0)
     _ < (∑ i ∈ range n, i)! := ?_
     _ ≤ k ! := by gcongr
   clear h h2
-  induction' n, hn using Nat.le_induction with n' hn' IH
-  · decide
-  let A := ∑ i ∈ range n', i
-  have le_sum : ∑ i ∈ range 6, i ≤ A := by
-    apply sum_le_sum_of_subset
-    simpa using hn'
-  calc 2 ^ ((n' + 1) * (n' + 1))
-      ≤ 2 ^ (n' * n' + 4 * n') := by gcongr <;> linarith
-    _ = 2 ^ (n' * n') * (2 ^ 4) ^ n' := by rw [← pow_mul, ← pow_add]
-    _ < A ! * (2 ^ 4) ^ n' := by gcongr
-    _ = A ! * (15 + 1) ^ n' := rfl
-    _ ≤ A ! * (A + 1) ^ n' := by gcongr; exact le_sum
-    _ ≤ (A + n')! := factorial_mul_pow_le_factorial
-    _ = (∑ i ∈ range (n' + 1), i)! := by rw [sum_range_succ]
+  induction n, hn using Nat.le_induction with
+  | base => decide
+  | succ n' hn' IH =>
+    let A := ∑ i ∈ range n', i
+    have le_sum : ∑ i ∈ range 6, i ≤ A := by
+      apply sum_le_sum_of_subset
+      simpa using hn'
+    calc 2 ^ ((n' + 1) * (n' + 1))
+        ≤ 2 ^ (n' * n' + 4 * n') := by gcongr <;> linarith
+      _ = 2 ^ (n' * n') * (2 ^ 4) ^ n' := by rw [← pow_mul, ← pow_add]
+      _ < A ! * (2 ^ 4) ^ n' := by gcongr
+      _ = A ! * (15 + 1) ^ n' := rfl
+      _ ≤ A ! * (A + 1) ^ n' := by gcongr; exact le_sum
+      _ ≤ (A + n')! := factorial_mul_pow_le_factorial
+      _ = (∑ i ∈ range (n' + 1), i)! := by rw [sum_range_succ]
 
 end Imo2019Q4
 

Archive/Imo/Imo2024Q1.lean

@@ -99,12 +99,14 @@ lemma mem_Ico_one_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) : α ∈ Set.Ico 1 2 := by
 lemma mem_Ico_n_of_mem_Ioo (h : α ∈ Set.Ioo 0 2) {n : ℕ} (hn : 0 < n) :
     α ∈ Set.Ico ((2 * n - 1) / n : ℝ) 2 := by
   suffices ∑ i ∈ Finset.Icc 1 n, ⌊i * α⌋ = n ^ 2 ∧ α ∈ Set.Ico ((2 * n - 1) / n : ℝ) 2 from this.2
-  induction' n, hn using Nat.le_induction with k kpos hk
-  · obtain ⟨h1, h2⟩ := hc.mem_Ico_one_of_mem_Ioo h
+  induction n, hn using Nat.le_induction with
+  | base =>
+    obtain ⟨h1, h2⟩ := hc.mem_Ico_one_of_mem_Ioo h
     simp only [zero_add, Finset.Icc_self, Finset.sum_singleton, Nat.cast_one, one_mul, one_pow,
                Int.floor_eq_iff, Int.cast_one, mul_one, div_one, Set.mem_Ico, tsub_le_iff_right]
     exact ⟨⟨h1, by linarith⟩, by linarith, h2⟩
-  · rcases hk with ⟨hks, hkl, hk2⟩
+  | succ k kpos hk =>
+    rcases hk with ⟨hks, hkl, hk2⟩
     have hs : (∑ i ∈ Finset.Icc 1 (k + 1), ⌊i * α⌋) =
          ⌊(k + 1 : ℕ) * α⌋ + ((k : ℕ) : ℤ) ^ 2 := by
       have hn11 : k + 1 ∉ Finset.Icc 1 k := by

Archive/MiuLanguage/DecisionSuf.lean

@@ -53,10 +53,9 @@ open MiuAtom List Nat
 where `count I w` is a power of 2.
 -/
 private theorem der_cons_replicate (n : ℕ) : Derivable (M :: replicate (2 ^ n) I) := by
-  induction' n with k hk
-  · -- base case
-    constructor
-  · -- inductive step
+  induction n with
+  | zero => constructor
+  | succ k hk =>
     rw [pow_add, pow_one 2, mul_two, replicate_add]
     exact Derivable.r2 hk
 
@@ -84,10 +83,12 @@ to produce another `Derivable` `Miustr`.
 -/
 theorem der_of_der_append_replicate_U_even {z : Miustr} {m : ℕ}
     (h : Derivable (z ++ ↑(replicate (m * 2) U))) : Derivable z := by
-  induction' m with k hk
-  · revert h
+  induction m with
+  | zero =>
+    revert h
     rw [replicate, append_nil]; exact id
-  · apply hk
+  | succ k hk =>
+    apply hk
     simp only [succ_mul, replicate_add] at h
     rw [← append_nil ↑(z ++ ↑(replicate (k * 2) U))]
     apply Derivable.r4
@@ -109,9 +110,11 @@ theorem der_cons_replicate_I_replicate_U_append_of_der_cons_replicate_I_append (
     (hder : Derivable (↑(M :: replicate (c + 3 * k) I) ++ xs)) :
     Derivable (↑(M :: (replicate c I ++ replicate k U)) ++ xs) := by
   revert xs
-  induction' k with a ha
-  · simp only [replicate, zero_eq, mul_zero, add_zero, append_nil, forall_true_iff, imp_self]
-  · intro xs
+  induction k with
+  | zero =>
+    simp only [replicate, zero_eq, mul_zero, add_zero, append_nil, forall_true_iff, imp_self]
+  | succ a ha =>
+    intro xs
     specialize ha (U :: xs)
     intro h₂
     -- We massage the goal into a form amenable to the application of `ha`.
@@ -141,18 +144,20 @@ theorem add_mod2 (a : ℕ) : ∃ t, a + a % 2 = t * 2 := by
 
 private theorem le_pow2_and_pow2_eq_mod3' (c : ℕ) (x : ℕ) (h : c = 1 ∨ c = 2) :
     ∃ m : ℕ, c + 3 * x ≤ 2 ^ m ∧ 2 ^ m % 3 = c % 3 := by
-  induction' x with k hk
-  · use c + 1
+  induction x with
+  | zero =>
+    use c + 1
     rcases h with hc | hc <;> · rw [hc]; norm_num
-  rcases hk with ⟨g, hkg, hgmod⟩
-  by_cases hp : c + 3 * (k + 1) ≤ 2 ^ g
-  · use g, hp, hgmod
-  refine ⟨g + 2, ?_, ?_⟩
-  · rw [mul_succ, ← add_assoc, pow_add]
-    change c + 3 * k + 3 ≤ 2 ^ g * (1 + 3); rw [mul_add (2 ^ g) 1 3, mul_one]
-    linarith [hkg, @Nat.one_le_two_pow g]
-  · rw [pow_add, ← mul_one c]
-    exact ModEq.mul hgmod rfl
+  | succ k hk =>
+    rcases hk with ⟨g, hkg, hgmod⟩
+    by_cases hp : c + 3 * (k + 1) ≤ 2 ^ g
+    · use g, hp, hgmod
+    refine ⟨g + 2, ?_, ?_⟩
+    · rw [mul_succ, ← add_assoc, pow_add]
+      change c + 3 * k + 3 ≤ 2 ^ g * (1 + 3); rw [mul_add (2 ^ g) 1 3, mul_one]
+      linarith [hkg, @Nat.one_le_two_pow g]
+    · rw [pow_add, ← mul_one c]
+      exact ModEq.mul hgmod rfl
 
 /-- If `a` is 1 or 2 modulo 3, then exists `k` a power of 2 for which `a ≤ k` and `a ≡ k [MOD 3]`.
 -/
@@ -245,9 +250,10 @@ conditions under which `count I ys = length ys`.
 -/
 theorem count_I_eq_length_of_count_U_zero_and_neg_mem {ys : Miustr} (hu : count U ys = 0)
     (hm : M ∉ ys) : count I ys = length ys := by
-  induction' ys with x xs hxs
-  · rfl
-  · cases x
+  induction ys with
+  | nil => rfl
+  | cons x xs hxs =>
+    cases x
     · -- case `x = M` gives a contradiction.
       exfalso; exact hm mem_cons_self
     · -- case `x = I`
@@ -282,9 +288,10 @@ relate to `count U`.
 
 
 theorem mem_of_count_U_eq_succ {xs : Miustr} {k : ℕ} (h : count U xs = succ k) : U ∈ xs := by
-  induction' xs with z zs hzs
-  · exfalso; rw [count] at h; contradiction
-  · rw [mem_cons]
+  induction xs with
+  | nil => exfalso; rw [count] at h; contradiction
+  | cons z zs hzs =>
+    rw [mem_cons]
     cases z <;> try exact Or.inl rfl
     all_goals right; simp only [count_cons, if_false] at h; exact hzs h
 
@@ -327,11 +334,10 @@ theorem der_of_decstr {en : Miustr} (h : Decstr en) : Derivable en := by
    for induction -/
   have hu : ∃ n, count U en = n := exists_eq'
   obtain ⟨n, hu⟩ := hu
-  revert en -- Crucially, we need the induction hypothesis to quantify over `en`
-  induction' n with k hk
-  · exact base_case_suf _
-  · intro ys hdec hus
-    rcases ind_hyp_suf k ys hus hdec with ⟨as, bs, hyab, habuc, hdecab⟩
+  induction n generalizing en with
+  | zero => exact base_case_suf _ h hu
+  | succ k hk =>
+    rcases ind_hyp_suf k en hu h with ⟨as, bs, hyab, habuc, hdecab⟩
     have h₂ : Derivable (↑(M :: as) ++ ↑[I, I, I] ++ bs) := hk hdecab habuc
     rw [hyab]
     exact Derivable.r3 h₂

Archive/OxfordInvariants/Summer2021/Week3P1.lean

@@ -89,10 +89,11 @@ theorem OxfordInvariants.Week3P1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤
   simp_rw [← @Nat.cast_pos α] at a_pos
   /- Declare the induction
     `ih` will be the induction hypothesis -/
-  induction' n with n ih
+  induction n with
+  | zero =>
   /- Base case
     Claim that the sum equals `1` -/
-  · refine ⟨1, ?_, ?_⟩
+    refine ⟨1, ?_, ?_⟩
     -- Check that this indeed equals the sum
     · rw [Nat.cast_one, Finset.sum_range_one]
       norm_num
@@ -101,6 +102,7 @@ theorem OxfordInvariants.Week3P1 (n : ℕ) (a : ℕ → ℕ) (a_pos : ∀ i ≤
     -- Check the divisibility condition
     · rw [mul_one, tsub_self]
       exact dvd_zero _
+  | succ n ih =>
   /- Induction step
     `b` is the value of the previous sum as a natural, `hb` is the proof that it is indeed the
     value, and `han` is the divisibility condition -/

Archive/Sensitivity.lean

@@ -199,9 +199,10 @@ variable {n : ℕ}
 
 open Classical in
 theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by
-  induction' n with n IH
-  · simp [Subsingleton.elim (α := Q 0) p q, ε, e]
-  · dsimp [ε, e]
+  induction n with
+  | zero => simp [Subsingleton.elim (α := Q 0) p q, ε, e]
+  | succ n IH =>
+    dsimp [ε, e]
     cases hp : p 0 <;> cases hq : q 0
     all_goals
       simp only [Bool.cond_true, Bool.cond_false, LinearMap.fst_apply, LinearMap.snd_apply,
@@ -210,9 +211,10 @@ theorem duality (p q : Q n) : ε p (e q) = if p = q then 1 else 0 := by
 
 /-- Any vector in `V n` annihilated by all `ε p`'s is zero. -/
 theorem epsilon_total {v : V n} (h : ∀ p : Q n, (ε p) v = 0) : v = 0 := by
-  induction' n with n ih
-  · dsimp [ε] at h; exact h fun _ => true
-  · obtain ⟨v₁, v₂⟩ := v
+  induction n with
+  | zero => dsimp [ε] at h; exact h fun _ => true
+  | succ n ih =>
+    obtain ⟨v₁, v₂⟩ := v
     ext <;> change _ = (0 : V n) <;> simp only <;> apply ih <;> intro p <;>
       [let q : Q n.succ := fun i => if h : i = 0 then true else p (i.pred h);
       let q : Q n.succ := fun i => if h : i = 0 then false else p (i.pred h)]
@@ -292,13 +294,13 @@ theorem f_squared (v : V n) : (f n) (f n v) = (n : ℝ) • v := by
 `q` the column index). -/
 
 open Classical in
-theorem f_matrix : ∀ p q : Q n, |ε q (f n (e p))| = if p ∈ q.adjacent then 1 else 0 := by
-  induction' n with n IH
-  · intro p q
+theorem f_matrix : ∀ p q : Q n, |ε q (f n (e p))| = if p ∈ q.adjacent then 1 else 0 := fun p q ↦ by
+  induction n with
+  | zero =>
     dsimp [f]
     simp [Q.not_adjacent_zero]
     rfl
-  · intro p q
+  | succ n IH =>
     have ite_nonneg : ite (π q = π p) (1 : ℝ) 0 ≥ 0 := by split_ifs <;> norm_num
     dsimp only [e, ε, f, V]; rw [LinearMap.prod_apply]; dsimp; cases hp : p 0 <;> cases hq : q 0
     all_goals