chore: fix yet more induction branch names (#23686)

Follow-up to #23448. This includes the entire stack of inductors in `Order.SuccPred.Limit`.

Author: Parcly-Taxel

Mathlib/AlgebraicTopology/RelativeCellComplex/Basic.lean

@@ -76,15 +76,15 @@ lemma hom_ext {Z : C} {φ₁ φ₂ : Y ⟶ Z} (h₀ : f ≫ φ₁ = f ≫ φ₂)
   refine c.isColimit.hom_ext (fun j ↦ ?_)
   dsimp
   induction j using SuccOrder.limitRecOn with
-  | hm j hj =>
+  | isMin j hj =>
     obtain rfl := hj.eq_bot
     simpa [← cancel_epi c.isoBot.inv] using h₀
-  | hs j hj hj' =>
+  | succ j hj hj' =>
     apply (c.attachCells j hj).hom_ext
     · simpa using hj'
     · intro i
       simpa only [Category.assoc, Cells.ι] using h ({ hj := hj, k := i, .. })
-  | hl j hj hj' =>
+  | isSuccLimit j hj hj' =>
     exact (c.F.isColimitOfIsWellOrderContinuous j hj).hom_ext
       (fun ⟨k, hk⟩ ↦ by simpa using hj' k hk)
 

Mathlib/CategoryTheory/Abelian/GrothendieckCategory/Monomorphisms.lean

@@ -34,14 +34,14 @@ namespace mono
 
 instance map_bot_le (j : J) : Mono (h.F.map (homOfLE bot_le : ⊥ ⟶ j)) := by
   induction j using SuccOrder.limitRecOn with
-  | hm j hj =>
+  | isMin j hj =>
     obtain rfl := hj.eq_bot
     exact inferInstanceAs (Mono (h.F.map (𝟙 _)))
-  | hs j hj hj' =>
+  | succ j hj hj' =>
     have : Mono _ := h.map_mem j hj
     rw [← homOfLE_comp bot_le (Order.le_succ j), Functor.map_comp]
     infer_instance
-  | hl j hj hj' =>
+  | isSuccLimit j hj hj' =>
     have : OrderBot (Set.Iio j) :=
       { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj ⟩
         bot_le _ := bot_le }

Mathlib/CategoryTheory/Limits/Shapes/Preorder/HasIterationOfShape.lean

@@ -73,10 +73,10 @@ lemma hasColimitsOfShape_of_initialSeg
   · let s := f.toPrincipalSeg hf
     obtain ⟨i, hi₀⟩ : ∃ i, i = s.top := ⟨_, rfl⟩
     induction i using SuccOrder.limitRecOn with
-    | hm i hi =>
+    | isMin i hi =>
       subst hi₀
       exact (hi.not_lt (s.lt_top (Classical.arbitrary _))).elim
-    | hs i hi _ =>
+    | succ i hi _ =>
       obtain ⟨a, rfl⟩ := (s.mem_range_iff_rel (b := i)).2 (by
         simpa only [← hi₀] using Order.lt_succ_of_not_isMax hi)
       have : OrderTop α :=
@@ -85,7 +85,7 @@ lemma hasColimitsOfShape_of_initialSeg
             rw [← s.le_iff_le]
             exact Order.le_of_lt_succ (by simpa only [hi₀] using s.lt_top b) }
       infer_instance
-    | hl i hi =>
+    | isSuccLimit i hi =>
       subst hi₀
       exact hasColimitsOfShape_of_isSuccLimit' C s hi
 

Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean

@@ -181,15 +181,15 @@ variable {X Y : C} {f : X ⟶ Y} (h : (isomorphisms C).TransfiniteCompositionOfS
 instance {j : J} (g : ⊥ ⟶ j) : IsIso (h.F.map g) := by
   obtain rfl : g = homOfLE bot_le := rfl
   induction j using SuccOrder.limitRecOn with
-  | hm j hj =>
+  | isMin j hj =>
     obtain rfl := hj.eq_bot
     dsimp
     infer_instance
-  | hs j hj hj' =>
+  | succ j hj hj' =>
     have : IsIso _ := h.map_mem j hj
     rw [← homOfLE_comp bot_le (Order.le_succ j), h.F.map_comp]
     infer_instance
-  | hl j hj hj' =>
+  | isSuccLimit j hj hj' =>
     letI : OrderBot (Set.Iio j) :=
       { bot := ⟨⊥, Order.IsSuccLimit.bot_lt hj⟩
         bot_le j := bot_le }

Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

@@ -359,49 +359,49 @@ instance subsingleton : Subsingleton (Φ.Iteration j) where
     suffices iter₁.F = iter₂.F by aesop
     revert iter₁ iter₂
     induction j using SuccOrder.limitRecOn with
-    | hm j h =>
-        obtain rfl := h.eq_bot
-        intro iter₁ iter₂
-        refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
-        obtain rfl : k₂ = ⊥ := by simpa using h₂
-        obtain rfl : k₁ = ⊥ := by simpa using h₁₂
-        apply mapEq_refl _ _ (by simp only [obj_bot])
-    | hs j hj₁ hj₂ =>
-        intro iter₁ iter₂
-        refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
-        have h₀ := Order.le_succ j
-        replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
-        have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
-        dsimp at hj₂ hsucc
-        wlog h : k₂ ≤ j generalizing k₁ k₂
-        · obtain h₂ | rfl := h₂.lt_or_eq
-          · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)
-          · by_cases h' : k₁ ≤ j
-            · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
-              simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
-                arrowSucc_eq, hsucc]
-            · simp only [not_le] at h'
-              obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
-                ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
-              rw [MapEq, arrowMap_refl, arrowMap_refl,
-                obj_succ _ _ h', obj_succ _ _ h', hsucc]
-        simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂]
-    | hl j h₁ h₂ =>
-        intro iter₁ iter₂
-        refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)
-        wlog h₄ : k₂ < j generalizing k₁ k₂; swap
-        · have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
-          simp at this
-          simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]
-        · obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
-          have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
-            Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
-          by_cases h₅ : k₁ < j
-          · dsimp [MapEq]
-            simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
-          · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
-            apply mapEq_refl
-            simp only [obj_limit _ _ h₁, this]
+    | isMin j h =>
+      obtain rfl := h.eq_bot
+      intro iter₁ iter₂
+      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
+      obtain rfl : k₂ = ⊥ := by simpa using h₂
+      obtain rfl : k₁ = ⊥ := by simpa using h₁₂
+      apply mapEq_refl _ _ (by simp only [obj_bot])
+    | succ j hj₁ hj₂ =>
+      intro iter₁ iter₂
+      refine ext (fun k₁ k₂ h₁₂ h₂ ↦ ?_)
+      have h₀ := Order.le_succ j
+      replace hj₂ := hj₂ (iter₁.trunc h₀) (iter₂.trunc h₀)
+      have hsucc := Functor.congr_obj hj₂ ⟨j, by simp⟩
+      dsimp at hj₂ hsucc
+      wlog h : k₂ ≤ j generalizing k₁ k₂
+      · obtain h₂ | rfl := h₂.lt_or_eq
+        · exact this _ _ _ _ ((Order.lt_succ_iff_of_not_isMax hj₁).1 h₂)
+        · by_cases h' : k₁ ≤ j
+          · apply mapEq_trans _ h₀ (this k₁ j h' h₀ (by simp))
+            simp only [MapEq, ← arrowSucc_def _ _ (Order.lt_succ_of_not_isMax hj₁),
+              arrowSucc_eq, hsucc]
+          · simp only [not_le] at h'
+            obtain rfl : k₁ = Order.succ j := le_antisymm h₁₂
+              ((Order.succ_le_iff_of_not_isMax hj₁).2 h')
+            rw [MapEq, arrowMap_refl, arrowMap_refl,
+              obj_succ _ _ h', obj_succ _ _ h', hsucc]
+      simp only [MapEq, ← arrowMap_restrictionLE _ (Order.le_succ j) _ _ _ h, hj₂]
+    | isSuccLimit j h₁ h₂ =>
+      intro iter₁ iter₂
+      refine ext (fun k₁ k₂ h₁₂ h₃ ↦ ?_)
+      wlog h₄ : k₂ < j generalizing k₁ k₂; swap
+      · have := h₂ k₂ h₄ (iter₁.trunc h₄.le) (iter₂.trunc h₄.le)
+        simp at this
+        simp only [MapEq, ← arrowMap_restrictionLE _ h₄.le _ _ _ (by rfl), this]
+      · obtain rfl : j = k₂ := le_antisymm (by simpa using h₄) h₃
+        have : restrictionLT iter₁.F le_rfl = restrictionLT iter₂.F le_rfl :=
+          Arrow.functor_ext (fun _ l _ ↦ this _ _ _ _ l.2)
+        by_cases h₅ : k₁ < j
+        · dsimp [MapEq]
+          simp_rw [arrowMap_limit _ _ h₁ _ _ h₅, this]
+        · obtain rfl : k₁ = j := le_antisymm h₁₂ (by simpa using h₅)
+          apply mapEq_refl
+          simp only [obj_limit _ _ h₁, this]
 
 lemma congr_obj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
     (k : J) (h₁ : k ≤ j₁) (h₂ : k ≤ j₂) :

Mathlib/CategoryTheory/SmallObject/Iteration/Nonempty.lean

@@ -142,11 +142,11 @@ variable (Φ)
 
 instance nonempty (j : J) : Nonempty (Φ.Iteration j) := by
   induction j using SuccOrder.limitRecOn with
-  | hm i hi =>
+  | isMin i hi =>
       obtain rfl : i = ⊥ := by simpa using hi
       exact ⟨mkOfBot Φ J⟩
-  | hs i hi hi' => exact ⟨mkOfSucc hi hi'.some⟩
-  | hl i hi hi' => exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩
+  | succ i hi hi' => exact ⟨mkOfSucc hi hi'.some⟩
+  | isSuccLimit i hi hi' => exact ⟨mkOfLimit hi (fun a ha ↦ (hi' a ha).some)⟩
 
 end Iteration
 

Mathlib/CategoryTheory/SmallObject/WellOrderInductionData.lean

@@ -112,33 +112,32 @@ lemma val_injective {j : J} {e e' : d.Extension val₀ j} (h : e.val = e'.val) :
 
 instance [WellFoundedLT J] (j : J) : Subsingleton (d.Extension val₀ j) := by
   induction j using SuccOrder.limitRecOn with
-  | hm i hi =>
-      obtain rfl : i = ⊥ := by simpa using hi
-      refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
-      have h₁ := e₁.map_zero
-      have h₂ := e₂.map_zero
-      simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply] at h₁ h₂
-      rw [h₁, h₂]
-  | hs i hi hi' =>
-      refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
-      have h₁ := e₁.map_succ i (Order.lt_succ_of_not_isMax hi)
-      have h₂ := e₂.map_succ i (Order.lt_succ_of_not_isMax hi)
-      simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply, homOfLE_leOfHom] at h₁ h₂
-      rw [h₁, h₂]
-      congr
-      exact congr_arg val
-        (Subsingleton.elim (e₁.ofLE (Order.le_succ i)) (e₂.ofLE (Order.le_succ i)))
-  | hl i hi hi' =>
-      refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
-      have h₁ := e₁.map_limit i hi (by rfl)
-      have h₂ := e₂.map_limit i hi (by rfl)
-      simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply, OrderHom.Subtype.val_coe,
-        comp_obj, op_obj, Monotone.functor_obj, homOfLE_leOfHom] at h₁ h₂
-      rw [h₁, h₂]
-      congr
-      ext ⟨⟨l, hl⟩⟩
-      have := hi' l hl
-      exact congr_arg val (Subsingleton.elim (e₁.ofLE hl.le) (e₂.ofLE hl.le))
+  | isMin i hi =>
+    obtain rfl : i = ⊥ := by simpa using hi
+    refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
+    have h₁ := e₁.map_zero
+    have h₂ := e₂.map_zero
+    simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply] at h₁ h₂
+    rw [h₁, h₂]
+  | succ i hi hi' =>
+    refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
+    have h₁ := e₁.map_succ i (Order.lt_succ_of_not_isMax hi)
+    have h₂ := e₂.map_succ i (Order.lt_succ_of_not_isMax hi)
+    simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply, homOfLE_leOfHom] at h₁ h₂
+    rw [h₁, h₂]
+    congr
+    exact congr_arg val (Subsingleton.elim (e₁.ofLE (Order.le_succ i)) (e₂.ofLE (Order.le_succ i)))
+  | isSuccLimit i hi hi' =>
+    refine Subsingleton.intro (fun e₁ e₂ ↦ val_injective ?_)
+    have h₁ := e₁.map_limit i hi (by rfl)
+    have h₂ := e₂.map_limit i hi (by rfl)
+    simp only [homOfLE_refl, op_id, FunctorToTypes.map_id_apply, OrderHom.Subtype.val_coe,
+      comp_obj, op_obj, Monotone.functor_obj, homOfLE_leOfHom] at h₁ h₂
+    rw [h₁, h₂]
+    congr
+    ext ⟨⟨l, hl⟩⟩
+    have := hi' l hl
+    exact congr_arg val (Subsingleton.elim (e₁.ofLE hl.le) (e₂.ofLE hl.le))
 
 lemma compatibility [WellFoundedLT J]
     {j : J} (e : d.Extension val₀ j) {i : J} (e' : d.Extension val₀ i) (h : i ≤ j) :
@@ -237,11 +236,11 @@ def limit (j : J) (hj : Order.IsSuccLimit j)
 
 instance (j : J) : Nonempty (d.Extension val₀ j) := by
   induction j using SuccOrder.limitRecOn with
-  | hm i hi =>
-      obtain rfl : i = ⊥ := by simpa using hi
-      exact ⟨zero d val₀⟩
-  | hs i hi hi' => exact ⟨hi'.some.succ hi⟩
-  | hl i hi hi' => exact ⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩
+  | isMin i hi =>
+    obtain rfl : i = ⊥ := by simpa using hi
+    exact ⟨zero d val₀⟩
+  | succ i hi hi' => exact ⟨hi'.some.succ hi⟩
+  | isSuccLimit i hi hi' => exact ⟨limit i hi (fun l hl ↦ (hi' l hl).some)⟩
 
 noncomputable instance (j : J) : Unique (d.Extension val₀ j) :=
   uniqueOfSubsingleton (Nonempty.some inferInstance)

Mathlib/Computability/TuringMachine.lean

@@ -421,18 +421,19 @@ def stWrite {k : K} (v : σ) (l : List (Γ k)) : StAct K Γ σ k → List (Γ k)
 of the stack, and all other actions, which do not. This is a modified recursor which lumps the
 stack actions into one. -/
 @[elab_as_elim]
-def stmtStRec.{l} {C : TM2.Stmt Γ Λ σ → Sort l} (H₁ : ∀ (k) (s : StAct K Γ σ k) (q)
-    (_ : C q), C (stRun s q))
-    (H₂ : ∀ (a q) (_ : C q), C (TM2.Stmt.load a q))
-    (H₃ : ∀ (p q₁ q₂) (_ : C q₁) (_ : C q₂), C (TM2.Stmt.branch p q₁ q₂))
-    (H₄ : ∀ l, C (TM2.Stmt.goto l)) (H₅ : C TM2.Stmt.halt) : ∀ n, C n
-  | TM2.Stmt.push _ f q => H₁ _ (push f) _ (stmtStRec H₁ H₂ H₃ H₄ H₅ q)
-  | TM2.Stmt.peek _ f q => H₁ _ (peek f) _ (stmtStRec H₁ H₂ H₃ H₄ H₅ q)
-  | TM2.Stmt.pop _ f q => H₁ _ (pop f) _ (stmtStRec H₁ H₂ H₃ H₄ H₅ q)
-  | TM2.Stmt.load _ q => H₂ _ _ (stmtStRec H₁ H₂ H₃ H₄ H₅ q)
-  | TM2.Stmt.branch _ q₁ q₂ => H₃ _ _ _ (stmtStRec H₁ H₂ H₃ H₄ H₅ q₁) (stmtStRec H₁ H₂ H₃ H₄ H₅ q₂)
-  | TM2.Stmt.goto _ => H₄ _
-  | TM2.Stmt.halt => H₅
+def stmtStRec.{l} {motive : TM2.Stmt Γ Λ σ → Sort l}
+    (run : ∀ (k) (s : StAct K Γ σ k) (q) (_ : motive q), motive (stRun s q))
+    (load : ∀ (a q) (_ : motive q), motive (TM2.Stmt.load a q))
+    (branch : ∀ (p q₁ q₂) (_ : motive q₁) (_ : motive q₂), motive (TM2.Stmt.branch p q₁ q₂))
+    (goto : ∀ l, motive (TM2.Stmt.goto l)) (halt : motive TM2.Stmt.halt) : ∀ n, motive n
+  | TM2.Stmt.push _ f q => run _ (push f) _ (stmtStRec run load branch goto halt q)
+  | TM2.Stmt.peek _ f q => run _ (peek f) _ (stmtStRec run load branch goto halt q)
+  | TM2.Stmt.pop _ f q => run _ (pop f) _ (stmtStRec run load branch goto halt q)
+  | TM2.Stmt.load _ q => load _ _ (stmtStRec run load branch goto halt q)
+  | TM2.Stmt.branch _ q₁ q₂ =>
+    branch _ _ _ (stmtStRec run load branch goto halt q₁) (stmtStRec run load branch goto halt q₂)
+  | TM2.Stmt.goto _ => goto _
+  | TM2.Stmt.halt => halt
 
 theorem supports_run (S : Finset Λ) {k : K} (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ) :
     TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q := by
@@ -680,14 +681,14 @@ theorem tr_respects : Respects (TM2.step M) (TM1.step (tr M)) TrCfg := by
   simp only [tr]
   generalize M l = N
   induction N using stmtStRec generalizing v S L hT with
-  | H₁ k s q IH => exact tr_respects_aux M hT s @IH
-  | H₂ a _ IH => exact IH _ hT
-  | H₃ p q₁ q₂ IH₁ IH₂ =>
+  | run k s q IH => exact tr_respects_aux M hT s @IH
+  | load a _ IH => exact IH _ hT
+  | branch p q₁ q₂ IH₁ IH₂ =>
     unfold TM2.stepAux trNormal TM1.stepAux
     beta_reduce
     cases p v <;> [exact IH₂ _ hT; exact IH₁ _ hT]
-  | H₄ => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
-  | H₅ => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
+  | goto => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
+  | halt => exact ⟨_, ⟨_, hT⟩, ReflTransGen.refl⟩
 
 section
 variable [Inhabited Λ] [Inhabited σ]

Mathlib/Order/DirectedInverseSystem.lean

@@ -416,7 +416,7 @@ theorem unique_pEquivOn (hs : IsLowerSet s) {e₁ e₂ : PEquivOn f equivSucc s}
   obtain ⟨e₁, nat₁, compat₁⟩ := e₁
   obtain ⟨e₂, nat₂, compat₂⟩ := e₂
   ext1; ext1 i; dsimp only
-  refine SuccOrder.prelimitRecOn i.1 (C := fun i ↦ ∀ h : i ∈ s, e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩)
+  refine SuccOrder.prelimitRecOn i.1 (motive := fun i ↦ ∀ h : i ∈ s, e₁ ⟨i, h⟩ = e₂ ⟨i, h⟩)
     (fun i nmax ih hi ↦ ?_) (fun i lim ih hi ↦ ?_) i.2
   · ext x ⟨j, hj⟩
     obtain rfl | hj := ((lt_succ_iff_of_not_isMax nmax).mp hj).eq_or_lt

Mathlib/Order/IsNormal.lean

@@ -49,13 +49,13 @@ theorem of_succ_lt [SuccOrder α] [WellFoundedLT α]
     IsNormal f := by
   refine ⟨fun a b ↦ ?_, hl⟩
   induction b using SuccOrder.limitRecOn with
-  | hm b hb => exact hb.not_lt.elim
-  | hs b hb IH =>
+  | isMin b hb => exact hb.not_lt.elim
+  | succ b hb IH =>
     intro hab
     obtain rfl | h := (lt_succ_iff_eq_or_lt_of_not_isMax hb).1 hab
     · exact hs a
     · exact (IH h).trans (hs b)
-  | hl b hb IH =>
+  | isSuccLimit b hb IH =>
     intro hab
     have hab' := hb.succ_lt hab
     exact (IH _ hab' (lt_succ_of_not_isMax hab.not_isMax)).trans_le