chore(Data/Fin/Tuple/Basic): rename recursor arguments (#35703)

Author: plp127

Mathlib/Data/Fin/Tuple/Basic.lean

@@ -179,14 +179,15 @@ def consEquiv (α : Fin (n + 1) → Type*) : α 0 × (∀ i, α (succ i)) ≃ 
 
 /-- Recurse on an `n+1`-tuple by splitting it into a single element and an `n`-tuple. -/
 @[elab_as_elim]
-def consCases {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x))
-    (x : ∀ i : Fin n.succ, α i) : P x :=
-  _root_.cast (by rw [cons_self_tail]) <| h (x 0) (tail x)
+def consCases {motive : (∀ i : Fin n.succ, α i) → Sort v} (cons : ∀ x₀ x, motive (Fin.cons x₀ x))
+    (x : ∀ i : Fin n.succ, α i) : motive x :=
+  _root_.cast (by rw [cons_self_tail]) <| cons (x 0) (tail x)
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
-theorem consCases_cons {P : (∀ i : Fin n.succ, α i) → Sort v} (h : ∀ x₀ x, P (Fin.cons x₀ x))
-    (x₀ : α 0) (x : ∀ i : Fin n, α i.succ) : consCases h (cons x₀ x) = h x₀ x := by
+theorem consCases_cons {motive : (∀ i : Fin n.succ, α i) → Sort v}
+    (cons : ∀ x₀ x, motive (Fin.cons x₀ x))
+    (x₀ : α 0) (x : ∀ i : Fin n, α i.succ) : consCases cons (Fin.cons x₀ x) = cons x₀ x := by
   rw [consCases, cast_eq]
   congr
 
@@ -710,25 +711,26 @@ def snocEquiv (α : Fin (n + 1) → Type*) : α (last n) × (∀ i, α (castSucc
 
 /-- Recurse on an `n+1`-tuple by splitting it its initial `n`-tuple and its last element. -/
 @[elab_as_elim, inline]
-def snocCases {P : (∀ i : Fin n.succ, α i) → Sort*}
-    (h : ∀ xs x, P (Fin.snoc xs x))
-    (x : ∀ i : Fin n.succ, α i) : P x :=
-  _root_.cast (by rw [Fin.snoc_init_self]) <| h (Fin.init x) (x <| Fin.last _)
+def snocCases {motive : (∀ i : Fin n.succ, α i) → Sort*}
+    (snoc : ∀ xs x, motive (Fin.snoc xs x))
+    (x : ∀ i : Fin n.succ, α i) : motive x :=
+  _root_.cast (by rw [Fin.snoc_init_self]) <| snoc (Fin.init x) (x <| Fin.last _)
 
 @[simp] lemma snocCases_snoc
-    {P : (∀ i : Fin (n + 1), α i) → Sort*} (h : ∀ x x₀, P (Fin.snoc x x₀))
+    {motive : (∀ i : Fin (n + 1), α i) → Sort*} (snoc : ∀ x x₀, motive (Fin.snoc x x₀))
     (x : ∀ i : Fin n, (Fin.init α) i) (x₀ : α (Fin.last _)) :
-    snocCases h (Fin.snoc x x₀) = h x x₀ := by
+    snocCases snoc (Fin.snoc x x₀) = snoc x x₀ := by
   rw [snocCases, cast_eq_iff_heq, Fin.init_snoc, Fin.snoc_last]
 
 /-- Recurse on a tuple by splitting into `Fin.elim0` and `Fin.snoc`. -/
 @[elab_as_elim]
 def snocInduction {α : Sort*}
-    {P : ∀ {n : ℕ}, (Fin n → α) → Sort*}
-    (h0 : P Fin.elim0)
-    (h : ∀ {n} (x : Fin n → α) (x₀), P x → P (Fin.snoc x x₀)) : ∀ {n : ℕ} (x : Fin n → α), P x
-  | 0, x => by convert h0
-  | _ + 1, x => snocCases (fun _ _ ↦ h _ _ <| snocInduction h0 h _) x
+    {motive : ∀ {n : ℕ}, (Fin n → α) → Sort*}
+    (elim0 : motive Fin.elim0)
+    (snoc : ∀ {n} (x : Fin n → α) (x₀), motive x → motive (Fin.snoc x x₀)) :
+    ∀ {n : ℕ} (x : Fin n → α), motive x
+  | 0, x => by convert elim0
+  | _ + 1, x => snocCases (fun _ _ ↦ snoc _ _ <| snocInduction elim0 snoc _) x
 
 theorem snoc_injective_of_injective {α} {x₀ : α} {x : Fin n → α}
     (hx : Function.Injective x) (hx₀ : x₀ ∉ Set.range x) :

Mathlib/Topology/Connected/PathConnected.lean

@@ -465,11 +465,11 @@ theorem IsPathConnected.exists_path_through_family {n : ℕ}
     Path.target_mem_range, and_true] at hp ⊢
   obtain ⟨hp, hx⟩ := hp
   induction p using snocInduction generalizing x with
-  | h0 =>
+  | elim0 =>
     simp only [snoc_zero]
     use Path.refl x
     simp [hx]
-  | @h n p y hp₂ =>
+  | @snoc n p y hp₂ =>
     simp only [forall_fin_succ', snoc_castSucc, snoc_last, snoc_apply_zero, Path.cast_coe] at hp ⊢
     obtain ⟨hp, hy⟩ := hp
     specialize hp₂ y hp hy