chore: deprime induction in AlgebraicTopology/CategoryTheory (leanprover-community#25774)

Most replacements that are also in leanprover-community#23676 have been copied over, but some have been optimised further.

Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

Author: Parcly-Taxel

Mathlib/AlgebraicTopology/DoldKan/Decomposition.lean

@@ -50,10 +50,12 @@ the $y_i$ are in degree $n$. -/
 theorem decomposition_Q (n q : ℕ) :
     ((Q q).f (n + 1) : X _⦋n + 1⦌ ⟶ X _⦋n + 1⦌) =
       ∑ i : Fin (n + 1) with i.val < q, (P i).f (n + 1) ≫ X.δ i.rev.succ ≫ X.σ (Fin.rev i) := by
-  induction' q with q hq
-  · simp only [Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero,
+  induction q with
+  | zero =>
+    simp only [Q_zero, HomologicalComplex.zero_f_apply, Nat.not_lt_zero,
       Finset.filter_false, Finset.sum_empty]
-  · by_cases hqn : q + 1 ≤ n + 1
+  | succ q hq =>
+    by_cases hqn : q + 1 ≤ n + 1
     swap
     · rw [Q_is_eventually_constant (show n + 1 ≤ q by omega), hq]
       congr 1

Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

@@ -53,18 +53,12 @@ theorem HigherFacesVanish.comp_σ {Y : C} {X : SimplicialObject C} {n b q : ℕ}
 
 theorem σ_comp_P_eq_zero (X : SimplicialObject C) {n q : ℕ} (i : Fin (n + 1)) (hi : n + 1 ≤ i + q) :
     X.σ i ≫ (P q).f (n + 1) = 0 := by
-  revert i hi
-  induction' q with q hq
-  · intro i (hi : n + 1 ≤ i)
-    omega
-  · intro i (hi : n + 1 ≤ i + q + 1)
+  induction q generalizing i with
+  | zero => omega
+  | succ q hq =>
     by_cases h : n + 1 ≤ (i : ℕ) + q
     · rw [P_succ, HomologicalComplex.comp_f, ← assoc, hq i h, zero_comp]
-    · replace hi : n = i + q := by
-        obtain ⟨j, hj⟩ := le_iff_exists_add.mp hi
-        rw [← Nat.lt_succ_iff, Nat.succ_eq_add_one, hj, not_lt, add_le_iff_nonpos_right,
-          nonpos_iff_eq_zero] at h
-        rw [← add_left_inj 1, hj, left_eq_add, h]
+    · replace hi : n = i + q := by omega
       rcases n with _ | n
       · fin_cases i
         dsimp at h hi

Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

@@ -36,7 +36,7 @@ variable {C : Type*} [Category C] [Preadditive C]
 theorem PInfty_comp_map_mono_eq_zero (X : SimplicialObject C) {n : ℕ} {Δ' : SimplexCategory}
     (i : Δ' ⟶ ⦋n⦌) [hi : Mono i] (h₁ : Δ'.len ≠ n) (h₂ : ¬Isδ₀ i) :
     PInfty.f n ≫ X.map i.op = 0 := by
-  induction' Δ' using SimplexCategory.rec with m
+  induction Δ' using SimplexCategory.rec with | _ m
   obtain ⟨k, hk⟩ := Nat.exists_eq_add_of_lt (len_lt_of_mono i fun h => by
         rw [← h] at h₁
         exact h₁ rfl)
@@ -78,8 +78,8 @@ theorem Γ₀_obj_termwise_mapMono_comp_PInfty (X : SimplicialObject C) {Δ Δ'
     (i : Δ ⟶ Δ') [Mono i] :
     Γ₀.Obj.Termwise.mapMono (AlternatingFaceMapComplex.obj X) i ≫ PInfty.f Δ.len =
       PInfty.f Δ'.len ≫ X.map i.op := by
-  induction' Δ using SimplexCategory.rec with n
-  induction' Δ' using SimplexCategory.rec with n'
+  induction Δ using SimplexCategory.rec with | _ n
+  induction Δ' using SimplexCategory.rec with | _ n'
   dsimp
   -- We start with the case `i` is an identity
   by_cases h : n = n'

Mathlib/AlgebraicTopology/DoldKan/Projections.lean

@@ -53,9 +53,10 @@ lemma P_succ (q : ℕ) : (P (q+1) : K[X] ⟶ K[X]) = P q ≫ (𝟙 _ + Hσ q) :=
 /-- All the `P q` coincide with `𝟙 _` in degree 0. -/
 @[simp]
 theorem P_f_0_eq (q : ℕ) : ((P q).f 0 : X _⦋0⦌ ⟶ X _⦋0⦌) = 𝟙 _ := by
-  induction' q with q hq
-  · rfl
-  · simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
+  induction q with
+  | zero => rfl
+  | succ q hq =>
+    simp only [P_succ, HomologicalComplex.add_f_apply, HomologicalComplex.comp_f,
       HomologicalComplex.id_f, id_comp, hq, Hσ_eq_zero, add_zero]
 
 /-- `Q q` is the complement projection associated to `P q` -/
@@ -95,10 +96,12 @@ theorem of_P : ∀ q n : ℕ, HigherFacesVanish q ((P q).f (n + 1) : X _⦋n + 1
 @[reassoc]
 theorem comp_P_eq_self {Y : C} {n q : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) :
     φ ≫ (P q).f (n + 1) = φ := by
-  induction' q with q hq
-  · simp only [P_zero]
+  induction q with
+  | zero =>
+    simp only [P_zero]
     apply comp_id
-  · simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
+  | succ q hq =>
+    simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
       comp_id, ← assoc, hq v.of_succ, add_eq_left]
     by_cases hqn : n < q
     · exact v.of_succ.comp_Hσ_eq_zero hqn
@@ -147,10 +150,12 @@ theorem Q_idem (q : ℕ) : (Q q : K[X] ⟶ K[X]) ≫ Q q = Q q := by
 def natTransP (q : ℕ) : alternatingFaceMapComplex C ⟶ alternatingFaceMapComplex C where
   app _ := P q
   naturality _ _ f := by
-    induction' q with q hq
-    · dsimp [alternatingFaceMapComplex]
+    induction q with
+    | zero =>
+      dsimp [alternatingFaceMapComplex]
       simp only [P_zero, id_comp, comp_id]
-    · simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
+    | succ q hq =>
+      simp only [P_succ, add_comp, comp_add, assoc, comp_id, hq, reassoc_of% hq]
       -- `erw` is needed to see through `natTransHσ q).app = Hσ q`
       erw [(natTransHσ q).naturality f]
       rfl
@@ -176,10 +181,12 @@ def natTransQ (q : ℕ) : alternatingFaceMapComplex C ⟶ alternatingFaceMapComp
 theorem map_P {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive]
     (X : SimplicialObject C) (q n : ℕ) :
     G.map ((P q : K[X] ⟶ _).f n) = (P q : K[((whiskering C D).obj G).obj X] ⟶ _).f n := by
-  induction' q with q hq
-  · simp only [P_zero]
+  induction q with
+  | zero =>
+    simp only [P_zero]
     apply G.map_id
-  · simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
+  | succ q hq =>
+    simp only [P_succ, comp_add, HomologicalComplex.comp_f, HomologicalComplex.add_f_apply,
       comp_id, Functor.map_add, Functor.map_comp, hq, map_Hσ]
 
 theorem map_Q {D : Type*} [Category D] [Preadditive D] (G : C ⥤ D) [G.Additive]

Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean

@@ -33,8 +33,8 @@ lemma Truncated.morphismProperty_eq_top
     W = ⊤ := by
   ext ⟨a, ha⟩ ⟨b, hb⟩ f
   simp only [MorphismProperty.top_apply, iff_true]
-  induction' a using SimplexCategory.rec with a
-  induction' b using SimplexCategory.rec with b
+  induction a using SimplexCategory.rec with | _ a
+  induction b using SimplexCategory.rec with | _ b
   dsimp at ha hb
   generalize h : a + b = c
   induction c generalizing a b with

Mathlib/AlgebraicTopology/SimplicialObject/Split.lean

@@ -85,9 +85,7 @@ instance : Fintype (IndexSet Δ) :=
         A.e.toOrderHom⟩ :
       IndexSet Δ → Sigma fun k : Fin (Δ.unop.len + 1) => Fin (Δ.unop.len + 1) → Fin (k + 1))
     (by
-      rintro ⟨Δ₁, α₁⟩ ⟨Δ₂, α₂⟩ h₁
-      induction' Δ₁ using Opposite.rec with Δ₁
-      induction' Δ₂ using Opposite.rec with Δ₂
+      rintro ⟨⟨Δ₁⟩, α₁⟩ ⟨⟨Δ₂⟩, α₂⟩ h₁
       simp only [unop_op, Sigma.mk.inj_iff, Fin.mk.injEq] at h₁
       have h₂ : Δ₁ = Δ₂ := by
         ext1
@@ -246,11 +244,10 @@ theorem hom_ext' {Z : C} {Δ : SimplexCategoryᵒᵖ} (f g : X.obj Δ ⟶ Z)
   Cofan.IsColimit.hom_ext (s.isColimit Δ) _ _ h
 
 theorem hom_ext (f g : X ⟶ Y) (h : ∀ n : ℕ, s.φ f n = s.φ g n) : f = g := by
-  ext Δ
+  ext ⟨Δ⟩
   apply s.hom_ext'
   intro A
-  induction' Δ using Opposite.rec with Δ
-  induction' Δ using SimplexCategory.rec with n
+  induction Δ using SimplexCategory.rec with | _ n
   dsimp
   simp only [s.cofan_inj_comp_app, h]
 

Mathlib/AlgebraicTopology/SimplicialSet/Degenerate.lean

@@ -114,7 +114,7 @@ lemma isIso_of_nonDegenerate (x : X.nonDegenerate n)
     (y : X.obj (op m)) (hy : X.map f.op y = x) :
     IsIso f := by
   obtain ⟨x, hx⟩ := x
-  induction' m using SimplexCategory.rec with m
+  induction m using SimplexCategory.rec with | _ m
   rw [mem_nonDegenerate_iff_notMem_degenerate] at hx
   by_contra!
   refine hx ⟨_, not_le.1 (fun h ↦ this ?_), f, y, hy⟩

Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean

@@ -84,7 +84,7 @@ in a nerve can be recovered from the underlying ReflPrefunctor. -/
 def toNerve₂.mk.app (n : SimplexCategory.Truncated 2) :
     X.obj (op n) ⟶ (nerveFunctor₂.obj (Cat.of C)).obj (op n) := by
   obtain ⟨n, hn⟩ := n
-  induction' n using SimplexCategory.rec with n
+  induction n using SimplexCategory.rec with | _ n
   match n with
   | 0 => exact fun x => .mk₀ (F.obj x)
   | 1 => exact fun f => .mk₁ (F.map ⟨f, rfl, rfl⟩)
@@ -297,7 +297,7 @@ theorem toNerve₂.ext (F G : X ⟶ nerveFunctor₂.obj (Cat.of C))
   have eq₁ (x : X _⦋1⦌₂) : F.app (op ⦋1⦌₂) x = G.app (op ⦋1⦌₂) x :=
     congr((($hyp).map ⟨x, rfl, rfl⟩).1)
   ext ⟨⟨n, hn⟩⟩ x
-  induction' n using SimplexCategory.rec with n
+  induction n using SimplexCategory.rec with | _ n
   match n with
   | 0 => apply eq₀
   | 1 => apply eq₁

Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean

@@ -210,7 +210,7 @@ lemma face_eq_ofSimplex {n : ℕ} (S : Finset (Fin (n + 1))) (m : ℕ) (e : Fin
           e.toOrderEmbedding.toOrderHom)) := by
   apply le_antisymm
   · rintro ⟨k⟩ x hx
-    induction' k using SimplexCategory.rec with k
+    induction k using SimplexCategory.rec with | _ k
     rw [mem_face_iff] at hx
     let φ : Fin (k + 1) →o S :=
       { toFun i := ⟨x i, hx i⟩
@@ -240,7 +240,7 @@ def faceRepresentableBy {n : ℕ} (S : Finset (Fin (n + 1)))
         ext i : 3
         apply e.symm_apply_apply
       right_inv := fun ⟨x, hx⟩ ↦ by
-        induction' j using SimplexCategory.rec with j
+        induction j using SimplexCategory.rec with | _ j
         dsimp
         ext i : 2
         exact congr_arg Subtype.val

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/EnoughInjectives.lean

@@ -134,7 +134,7 @@ lemma exists_pushouts
 lemma exists_larger_subobject {X : C} (A : Subobject X) (hA : A ≠ ⊤) :
     ∃ (A' : Subobject X) (h : A < A'),
       (generatingMonomorphisms G).pushouts (Subobject.ofLE A A' h.le) := by
-  induction' A using Subobject.ind with Y f _
+  induction A using Subobject.ind with | _ f
   obtain ⟨X', i, p', hi, hi', hp', fac⟩ := exists_pushouts hG f
     (by simpa only [Subobject.isIso_iff_mk_eq_top] using hA)
   refine ⟨Subobject.mk p', Subobject.mk_lt_mk_of_comm i fac hi',