chore: rename Fin.castSucc to Fin.castSuccEmb (#5729)

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

Mathlib/Algebra/BigOperators/Fin.lean

@@ -18,7 +18,7 @@ import Mathlib.Logic.Equiv.Fin
 
 Some results about products and sums over the type `Fin`.
 
-The most important results are the induction formulas `Fin.prod_univ_castSucc`
+The most important results are the induction formulas `Fin.prod_univ_castSuccEmb`
 and `Fin.prod_univ_succ`, and the formula `Fin.prod_const` for the product of a
 constant function. These results have variants for sums instead of products.
 
@@ -90,11 +90,11 @@ theorem prod_univ_succ [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
 is the product of `f (Fin.last n)` plus the remaining product -/
 @[to_additive "A sum of a function `f : Fin (n + 1) → β` over all `Fin (n + 1)` is the sum of
 `f (Fin.last n)` plus the remaining sum"]
-theorem prod_univ_castSucc [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
-    ∏ i, f i = (∏ i : Fin n, f (Fin.castSucc i)) * f (last n) := by
+theorem prod_univ_castSuccEmb [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
+    ∏ i, f i = (∏ i : Fin n, f (Fin.castSuccEmb i)) * f (last n) := by
   simpa [mul_comm] using prod_univ_succAbove f (last n)
-#align fin.prod_univ_cast_succ Fin.prod_univ_castSucc
-#align fin.sum_univ_cast_succ Fin.sum_univ_castSucc
+#align fin.prod_univ_cast_succ Fin.prod_univ_castSuccEmb
+#align fin.sum_univ_cast_succ Fin.sum_univ_castSuccEmb
 
 @[to_additive]
 theorem prod_cons [CommMonoid β] {n : ℕ} (x : β) (f : Fin n → β) :
@@ -116,46 +116,46 @@ theorem prod_univ_two [CommMonoid β] (f : Fin 2 → β) : ∏ i, f i = f 0 * f
 
 @[to_additive]
 theorem prod_univ_three [CommMonoid β] (f : Fin 3 → β) : ∏ i, f i = f 0 * f 1 * f 2 := by
-  rw [prod_univ_castSucc, prod_univ_two]
+  rw [prod_univ_castSuccEmb, prod_univ_two]
   rfl
 #align fin.prod_univ_three Fin.prod_univ_three
 #align fin.sum_univ_three Fin.sum_univ_three
 
 @[to_additive]
 theorem prod_univ_four [CommMonoid β] (f : Fin 4 → β) : ∏ i, f i = f 0 * f 1 * f 2 * f 3 := by
-  rw [prod_univ_castSucc, prod_univ_three]
+  rw [prod_univ_castSuccEmb, prod_univ_three]
   rfl
 #align fin.prod_univ_four Fin.prod_univ_four
 #align fin.sum_univ_four Fin.sum_univ_four
 
 @[to_additive]
 theorem prod_univ_five [CommMonoid β] (f : Fin 5 → β) :
     ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 := by
-  rw [prod_univ_castSucc, prod_univ_four]
+  rw [prod_univ_castSuccEmb, prod_univ_four]
   rfl
 #align fin.prod_univ_five Fin.prod_univ_five
 #align fin.sum_univ_five Fin.sum_univ_five
 
 @[to_additive]
 theorem prod_univ_six [CommMonoid β] (f : Fin 6 → β) :
     ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 := by
-  rw [prod_univ_castSucc, prod_univ_five]
+  rw [prod_univ_castSuccEmb, prod_univ_five]
   rfl
 #align fin.prod_univ_six Fin.prod_univ_six
 #align fin.sum_univ_six Fin.sum_univ_six
 
 @[to_additive]
 theorem prod_univ_seven [CommMonoid β] (f : Fin 7 → β) :
     ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 := by
-  rw [prod_univ_castSucc, prod_univ_six]
+  rw [prod_univ_castSuccEmb, prod_univ_six]
   rfl
 #align fin.prod_univ_seven Fin.prod_univ_seven
 #align fin.sum_univ_seven Fin.sum_univ_seven
 
 @[to_additive]
 theorem prod_univ_eight [CommMonoid β] (f : Fin 8 → β) :
     ∏ i, f i = f 0 * f 1 * f 2 * f 3 * f 4 * f 5 * f 6 * f 7 := by
-  rw [prod_univ_castSucc, prod_univ_seven]
+  rw [prod_univ_castSuccEmb, prod_univ_seven]
   rfl
 #align fin.prod_univ_eight Fin.prod_univ_eight
 #align fin.sum_univ_eight Fin.sum_univ_eight
@@ -231,7 +231,7 @@ theorem partialProd_zero (f : Fin n → α) : partialProd f 0 = 1 := by simp [pa
 
 @[to_additive]
 theorem partialProd_succ (f : Fin n → α) (j : Fin n) :
-    partialProd f j.succ = partialProd f (Fin.castSucc j) * f j := by
+    partialProd f j.succ = partialProd f (Fin.castSuccEmb j) * f j := by
   simp [partialProd, List.take_succ, List.ofFnNthVal, dif_pos j.is_lt, ← Option.coe_def]
 #align fin.partial_prod_succ Fin.partialProd_succ
 #align fin.partial_sum_succ Fin.partialSum_succ
@@ -248,23 +248,23 @@ theorem partialProd_succ' (f : Fin (n + 1) → α) (j : Fin (n + 1)) :
 theorem partialProd_left_inv {G : Type _} [Group G] (f : Fin (n + 1) → G) :
     (f 0 • partialProd fun i : Fin n => (f i)⁻¹ * f i.succ) = f :=
   funext fun x => Fin.inductionOn x (by simp) fun x hx => by
-    simp only [coe_eq_castSucc, Pi.smul_apply, smul_eq_mul] at hx ⊢
+    simp only [coe_eq_castSuccEmb, Pi.smul_apply, smul_eq_mul] at hx ⊢
     rw [partialProd_succ, ← mul_assoc, hx, mul_inv_cancel_left]
 #align fin.partial_prod_left_inv Fin.partialProd_left_inv
 #align fin.partial_sum_left_neg Fin.partialSum_left_neg
 
 @[to_additive]
 theorem partialProd_right_inv {G : Type _} [Group G] (f : Fin n → G) (i : Fin n) :
-    (partialProd f (Fin.castSucc i))⁻¹ * partialProd f i.succ = f i := by
+    (partialProd f (Fin.castSuccEmb i))⁻¹ * partialProd f i.succ = f i := by
   cases' i with i hn
   induction i with
   | zero => simp [-Fin.succ_mk, partialProd_succ]
   | succ i hi =>
     specialize hi (lt_trans (Nat.lt_succ_self i) hn)
-    simp only [Fin.coe_eq_castSucc, Fin.succ_mk, Fin.castSucc_mk] at hi ⊢
+    simp only [Fin.coe_eq_castSuccEmb, Fin.succ_mk, Fin.castSuccEmb_mk] at hi ⊢
     rw [← Fin.succ_mk _ _ (lt_trans (Nat.lt_succ_self _) hn), ← Fin.succ_mk]
     rw [Nat.succ_eq_add_one] at hn
-    simp only [partialProd_succ, mul_inv_rev, Fin.castSucc_mk]
+    simp only [partialProd_succ, mul_inv_rev, Fin.castSuccEmb_mk]
     -- Porting note: was
     -- assoc_rw [hi, inv_mul_cancel_left]
     rw [← mul_assoc, mul_left_eq_self, mul_assoc, hi, mul_left_inv]
@@ -284,20 +284,20 @@ Useful for defining group cohomology. -/
       Useful for defining group cohomology."]
 theorem inv_partialProd_mul_eq_contractNth {G : Type _} [Group G] (g : Fin (n + 1) → G)
     (j : Fin (n + 1)) (k : Fin n) :
-    (partialProd g (j.succ.succAbove (Fin.castSucc k)))⁻¹ * partialProd g (j.succAbove k).succ =
+    (partialProd g (j.succ.succAbove (Fin.castSuccEmb k)))⁻¹ * partialProd g (j.succAbove k).succ =
       j.contractNth (· * ·) g k := by
   rcases lt_trichotomy (k : ℕ) j with (h | h | h)
   · rwa [succAbove_below, succAbove_below, partialProd_right_inv, contractNth_apply_of_lt]
     · assumption
-    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
+    · rw [castSuccEmb_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
       exact le_of_lt h
-  · rwa [succAbove_below, succAbove_above, partialProd_succ, castSucc_fin_succ, ← mul_assoc,
+  · rwa [succAbove_below, succAbove_above, partialProd_succ, castSuccEmb_fin_succ, ← mul_assoc,
       partialProd_right_inv, contractNth_apply_of_eq]
     · simp [le_iff_val_le_val, ← h]
-    · rw [castSucc_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
+    · rw [castSuccEmb_lt_iff_succ_le, succ_le_succ_iff, le_iff_val_le_val]
       exact le_of_eq h
   · rwa [succAbove_above, succAbove_above, partialProd_succ, partialProd_succ,
-      castSucc_fin_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
+      castSuccEmb_fin_succ, partialProd_succ, inv_mul_cancel_left, contractNth_apply_of_gt]
     · exact le_iff_val_le_val.2 (le_of_lt h)
     · rw [le_iff_val_le_val, val_succ]
       exact Nat.succ_le_of_lt h
@@ -318,7 +318,7 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
       cases m
       · dsimp only [Nat.zero_eq] at f -- porting note: added, wrong zero
         exact isEmptyElim (f <| Fin.last _)
-      simp_rw [Fin.sum_univ_castSucc, Fin.coe_castSucc, Fin.val_last]
+      simp_rw [Fin.sum_univ_castSuccEmb, Fin.coe_castSuccEmb, Fin.val_last]
       refine' (add_lt_add_of_lt_of_le (ih _) <| mul_le_mul_right' (Fin.is_le _) _).trans_eq _
       rw [← one_add_mul (_ : ℕ), add_comm, pow_succ]
       -- porting note: added, wrong `succ`
@@ -364,15 +364,15 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
     (fun f => ⟨∑ i, f i * ∏ j, n (Fin.castLE i.is_lt.le j), by
       induction' m with m ih
       · simp
-      rw [Fin.prod_univ_castSucc, Fin.sum_univ_castSucc]
+      rw [Fin.prod_univ_castSuccEmb, Fin.sum_univ_castSuccEmb]
       suffices
         ∀ (n : Fin m → ℕ) (nn : ℕ) (f : ∀ i : Fin m, Fin (n i)) (fn : Fin nn),
           ((∑ i : Fin m, ↑(f i) * ∏ j : Fin i, n (Fin.castLE i.prop.le j)) + ↑fn * ∏ j, n j) <
             (∏ i : Fin m, n i) * nn by
         replace := this (Fin.init n) (n (Fin.last _)) (Fin.init f) (f (Fin.last _))
         rw [← Fin.snoc_init_self f]
         simp (config := { singlePass := true }) only [← Fin.snoc_init_self n]
-        simp_rw [Fin.snoc_castSucc, Fin.snoc_last, Fin.snoc_init_self n]
+        simp_rw [Fin.snoc_castSuccEmb, Fin.snoc_last, Fin.snoc_init_self n]
         exact this
       intro n nn f fn
       cases nn

Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

@@ -106,17 +106,17 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
     rintro ⟨i, j⟩ ⟨i', j'⟩ hij hij' h
     rw [Prod.mk.inj_iff]
     exact ⟨by simpa using congr_arg Prod.snd h,
-      by simpa [Fin.castSucc_castLT] using congr_arg Fin.castSucc (congr_arg Prod.fst h)⟩
+      by simpa [Fin.castSuccEmb_castLT] using congr_arg Fin.castSuccEmb (congr_arg Prod.fst h)⟩
   · -- φ : S → Sᶜ is surjective
     rintro ⟨i', j'⟩ hij'
     simp only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.compl_filter,
       not_le, Finset.mem_filter, true_and] at hij'
-    refine' ⟨(j'.pred _, Fin.castSucc i'), _, _⟩
+    refine' ⟨(j'.pred _, Fin.castSuccEmb i'), _, _⟩
     · rintro rfl
       simp only [Fin.val_zero, not_lt_zero'] at hij'
     · simpa only [Finset.mem_univ, forall_true_left, Prod.forall, ge_iff_le, Finset.mem_filter,
-        Fin.coe_castSucc, Fin.coe_pred, true_and] using Nat.le_pred_of_lt hij'
-    · simp only [Fin.castLT_castSucc, Fin.succ_pred]
+        Fin.coe_castSuccEmb, Fin.coe_pred, true_and] using Nat.le_pred_of_lt hij'
+    · simp only [Fin.castLT_castSuccEmb, Fin.succ_pred]
 #align algebraic_topology.alternating_face_map_complex.d_squared AlgebraicTopology.AlternatingFaceMapComplex.d_squared
 
 /-!

Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

@@ -88,7 +88,7 @@ theorem σ_comp_P_eq_zero (X : SimplicialObject C) {n q : ℕ} (i : Fin (n + 1))
         erw [SimplicialObject.δ_comp_σ_self, SimplicialObject.δ_comp_σ_self_assoc,
           SimplicialObject.δ_comp_σ_succ, comp_id,
           SimplicialObject.δ_comp_σ_of_le X
-            (show (0 : Fin 2) ≤ Fin.castSucc 0 by rw [Fin.castSucc_zero]),
+            (show (0 : Fin 2) ≤ Fin.castSuccEmb 0 by rw [Fin.castSuccEmb_zero]),
           SimplicialObject.δ_comp_σ_self_assoc, SimplicialObject.δ_comp_σ_succ_assoc]
         simp only [add_right_neg, add_zero, zero_add]
       · rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp,
@@ -103,9 +103,9 @@ theorem σ_comp_P_eq_zero (X : SimplicialObject C) {n q : ℕ} (i : Fin (n + 1))
         simp only [Nat.succ_eq_add_one] at hi
         obtain ⟨k, hk⟩ := Nat.le.dest (Nat.lt_succ_iff.mp (Fin.is_lt j))
         rw [add_comm] at hk
-        have hi' : i = Fin.castSucc ⟨i, by linarith⟩ := by
+        have hi' : i = Fin.castSuccEmb ⟨i, by linarith⟩ := by
           ext
-          simp only [Fin.castSucc_mk, Fin.eta]
+          simp only [Fin.castSuccEmb_mk, Fin.eta]
         have eq := hq j.revPerm.succ (by
           simp only [← hk, Fin.revPerm_eq j hk.symm, Nat.succ_eq_add_one, Fin.succ_mk, Fin.val_mk]
           linarith)

Mathlib/AlgebraicTopology/DoldKan/Faces.lean

@@ -107,8 +107,8 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
   simp only [assoc]
   conv_lhs =>
     congr
-    · rw [Fin.sum_univ_castSucc]
-    · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
+    · rw [Fin.sum_univ_castSuccEmb]
+    · rw [Fin.sum_univ_castSuccEmb, Fin.sum_univ_castSuccEmb]
   dsimp [Fin.castIso, Fin.castLE, Fin.castLT]
   /- the purpose of the following `simplif` is to create three subgoals in order
       to finish the proof -/
@@ -121,7 +121,7 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
     rw [← pow_add, Odd.neg_one_pow, neg_smul, one_zsmul]
     exact ⟨a, by linarith⟩
   · -- d + e = 0
-    rw [X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm,
+    rw [X.δ_comp_σ_self' (Fin.castSuccEmb_mk _ _ _).symm,
       X.δ_comp_σ_succ' (Fin.succ_mk _ _ _).symm]
     simp only [comp_id, pow_add _ (a + 1) 1, pow_one, mul_neg, mul_one, neg_mul, neg_smul,
       add_right_neg]
@@ -131,7 +131,7 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
     rintro ⟨i, hi⟩ _
     simp only
     have hia : (⟨i, by linarith⟩ : Fin (n + 2)) ≤
-        Fin.castSucc (⟨a, by linarith⟩ : Fin (n + 1)) := by
+        Fin.castSuccEmb (⟨a, by linarith⟩ : Fin (n + 1)) := by
       rw [Fin.le_iff_val_le_val]
       dsimp
       linarith
@@ -151,8 +151,8 @@ theorem comp_Hσ_eq_zero {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : Higher
       Fin.mk_zero, one_zsmul, eqToHom_refl, comp_id, comp_sum,
       AlternatingFaceMapComplex.obj_d_eq]
     rw [← Fin.sum_congr' _ (show 2 + (n + 1) = n + 1 + 2 by linarith), Fin.sum_trunc]
-    · simp only [Fin.sum_univ_castSucc, Fin.sum_univ_zero, zero_add, Fin.last, Fin.castLE_mk,
-        Fin.castIso_mk, Fin.castSucc_mk]
+    · simp only [Fin.sum_univ_castSuccEmb, Fin.sum_univ_zero, zero_add, Fin.last, Fin.castLE_mk,
+        Fin.castIso_mk, Fin.castSuccEmb_mk]
       simp only [Fin.mk_zero, Fin.val_zero, pow_zero, one_zsmul, Fin.mk_one, Fin.val_one, pow_one,
         neg_smul, comp_neg]
       erw [δ_comp_σ_self, δ_comp_σ_succ, add_right_neg]