diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean
index 9d54d5dfb5858..5ea28f4df10a4 100644
--- a/Mathlib/Algebra/BigOperators/Fin.lean
+++ b/Mathlib/Algebra/BigOperators/Fin.lean
@@ -187,7 +187,7 @@ theorem prod_Ioi_succ {M : Type _} [CommMonoid M] {n : ℕ} (i : Fin n) (v : Fin
 
 @[to_additive]
 theorem prod_congr' {M : Type _} [CommMonoid M] {a b : ℕ} (f : Fin b → M) (h : a = b) :
-    (∏ i : Fin a, f (cast h i)) = ∏ i : Fin b, f i := by
+    (∏ i : Fin a, f (castIso h i)) = ∏ i : Fin b, f i := by
   subst h
   congr
 #align fin.prod_congr' Fin.prod_congr'
@@ -334,7 +334,7 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
     fun a => by
       dsimp
       induction' n with n ih
-      · haveI : Subsingleton (Fin (m ^ 0)) := (Fin.cast <| pow_zero _).toEquiv.subsingleton
+      · haveI : Subsingleton (Fin (m ^ 0)) := (Fin.castIso <| pow_zero _).toEquiv.subsingleton
         exact Subsingleton.elim _ _
       simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
       ext
@@ -394,14 +394,14 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
       refine' Fin.consInduction _ _ n
       · intro a
         haveI : Subsingleton (Fin (∏ i : Fin 0, i.elim0)) :=
-          (Fin.cast <| prod_empty).toEquiv.subsingleton
+          (Fin.castIso <| prod_empty).toEquiv.subsingleton
         exact Subsingleton.elim _ _
       · intro n x xs ih a
         simp_rw [Fin.forall_iff, Fin.ext_iff] at ih
         ext
         simp_rw [Fin.sum_univ_succ, Fin.cons_succ]
         have := fun i : Fin n =>
-          Fintype.prod_equiv (Fin.cast <| Fin.val_succ i).toEquiv
+          Fintype.prod_equiv (Fin.castIso <| Fin.val_succ i).toEquiv
             (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Fin.is_lt _).le j))
             (fun j => (Fin.cons x xs : _ → ℕ) (Fin.castLE (Nat.succ_le_succ (Fin.is_lt _).le) j))
             fun j => rfl
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
index 8d3b81c70a451..7a8698cc683b2 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Faces.lean
@@ -85,7 +85,7 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
   swap
   · rintro ⟨k, hk⟩
     suffices φ ≫ X.δ (⟨a + 2 + k, by linarith⟩ : Fin (n + 2)) = 0 by
-      simp only [this, Fin.natAdd_mk, Fin.cast_mk, zero_comp, smul_zero]
+      simp only [this, Fin.natAdd_mk, Fin.castIso_mk, zero_comp, smul_zero]
     convert v ⟨a + k + 1, by linarith⟩ (by rw [Fin.val_mk] ; linarith)
     dsimp
     linarith
@@ -95,13 +95,13 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
   · rintro ⟨k, hk⟩
     rw [assoc, X.δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
     · simp only [Fin.lt_iff_val_lt_val]
-      dsimp [Fin.natAdd, Fin.cast]
+      dsimp [Fin.natAdd, Fin.castIso]
       linarith
     · intro h
       rw [Fin.pred_eq_iff_eq_succ, Fin.ext_iff] at h
-      dsimp [Fin.cast] at h
+      dsimp [Fin.castIso] at h
       linarith
-    · dsimp [Fin.cast, Fin.pred]
+    · dsimp [Fin.castIso, Fin.pred]
       rw [Nat.pred_eq_sub_one, Nat.succ_add_sub_one]
       linarith
   simp only [assoc]
@@ -109,7 +109,7 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
     congr
     · rw [Fin.sum_univ_castSucc]
     · rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-  dsimp [Fin.cast, Fin.castLE, Fin.castLT]
+  dsimp [Fin.castIso, Fin.castLE, Fin.castLT]
   /- the purpose of the following `simplif` is to create three subgoals in order
       to finish the proof -/
   have simplif :
@@ -152,12 +152,12 @@ theorem comp_Hσ_eq_zero {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : Higher
       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.cast_mk, Fin.castSucc_mk]
+        Fin.castIso_mk, Fin.castSucc_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]
     · intro j
-      dsimp [Fin.cast, Fin.castLE, Fin.castLT]
+      dsimp [Fin.castIso, Fin.castLE, Fin.castLT]
       rw [comp_zsmul, comp_zsmul, δ_comp_σ_of_gt', v.comp_δ_eq_zero_assoc, zero_comp, zsmul_zero]
       · simp only [Fin.lt_iff_val_lt_val]
         dsimp [Fin.succ]
diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean
index 7e97ef4d5d310..70c000fe2db4e 100644
--- a/Mathlib/Analysis/Analytic/Basic.lean
+++ b/Mathlib/Analysis/Analytic/Basic.lean
@@ -1177,7 +1177,7 @@ def changeOriginIndexEquiv :
   invFun s :=
     ⟨s.1 - s.2.card, s.2.card,
       ⟨s.2.map
-          (Fin.cast <| (tsub_add_cancel_of_le <| card_finset_fin_le s.2).symm).toEquiv.toEmbedding,
+        (Fin.castIso <| (tsub_add_cancel_of_le <| card_finset_fin_le s.2).symm).toEquiv.toEmbedding,
         Finset.card_map _⟩⟩
   left_inv := by
     rintro ⟨k, l, ⟨s : Finset (Fin <| k + l), hs : s.card = l⟩⟩
@@ -1185,15 +1185,15 @@ def changeOriginIndexEquiv :
     -- Lean can't automatically generalize `k' = k + l - s.card`, `l' = s.card`, so we explicitly
     -- formulate the generalized goal
     suffices ∀ k' l', k' = k → l' = l → ∀ (hkl : k + l = k' + l') (hs'),
-        (⟨k', l', ⟨Finset.map (Fin.cast hkl).toEquiv.toEmbedding s, hs'⟩⟩ :
+        (⟨k', l', ⟨Finset.map (Fin.castIso hkl).toEquiv.toEmbedding s, hs'⟩⟩ :
           Σk l : ℕ, { s : Finset (Fin (k + l)) // s.card = l }) = ⟨k, l, ⟨s, hs⟩⟩ by
       apply this <;> simp only [hs, add_tsub_cancel_right]
     rintro _ _ rfl rfl hkl hs'
-    simp only [Equiv.refl_toEmbedding, Fin.cast_refl, Finset.map_refl, eq_self_iff_true,
+    simp only [Equiv.refl_toEmbedding, Fin.castIso_refl, Finset.map_refl, eq_self_iff_true,
       OrderIso.refl_toEquiv, and_self_iff, heq_iff_eq]
   right_inv := by
     rintro ⟨n, s⟩
-    simp [tsub_add_cancel_of_le (card_finset_fin_le s), Fin.cast_to_equiv]
+    simp [tsub_add_cancel_of_le (card_finset_fin_le s), Fin.castIso_to_equiv]
 #align formal_multilinear_series.change_origin_index_equiv FormalMultilinearSeries.changeOriginIndexEquiv
 
 theorem changeOriginSeries_summable_aux₁ {r r' : ℝ≥0} (hr : (r + r' : ℝ≥0∞) < p.radius) :
@@ -1320,7 +1320,7 @@ theorem changeOrigin_eval (h : (‖x‖₊ + ‖y‖₊ : ℝ≥0∞) < p.radius
     changeOriginIndexEquiv_symm_apply_snd_fst, changeOriginIndexEquiv_symm_apply_snd_snd_coe]
   rw [ContinuousMultilinearMap.curryFinFinset_apply_const]
   have : ∀ (m) (hm : n = m), p n (s.piecewise (fun _ => x) fun _ => y) =
-      p m ((s.map (Fin.cast hm).toEquiv.toEmbedding).piecewise (fun _ => x) fun _ => y) := by
+      p m ((s.map (Fin.castIso hm).toEquiv.toEmbedding).piecewise (fun _ => x) fun _ => y) := by
     rintro m rfl
     simp [Finset.piecewise]
   apply this
diff --git a/Mathlib/Data/Fin/Basic.lean b/Mathlib/Data/Fin/Basic.lean
index 1d34958229382..53f48f335f6bf 100644
--- a/Mathlib/Data/Fin/Basic.lean
+++ b/Mathlib/Data/Fin/Basic.lean
@@ -52,7 +52,7 @@ This file expands on the development in the core library.
 * `Fin.valOrderEmbedding` : coercion to natural numbers as an `OrderEmbedding`;
 * `Fin.succEmbedding` : `Fin.succ` as an `OrderEmbedding`;
 * `Fin.castLE h` : embed `Fin n` into `Fin m`, `h : n ≤ m`;
-* `Fin.cast` : order isomorphism between `Fin n` and `Fin m` provided that `n = m`,
+* `Fin.castIso` : order isomorphism between `Fin n` and `Fin m` provided that `n = m`,
   see also `Equiv.finCongr`;
 * `Fin.castAdd m` : embed `Fin n` into `Fin (n+m)`;
 * `Fin.castSucc` : embed `Fin n` into `Fin (n+1)`;
@@ -1057,69 +1057,69 @@ theorem castLE_comp_castLE {k m n} (km : k ≤ m) (mn : m ≤ n) :
   funext (castLE_castLE km mn)
 #align fin.cast_le_comp_cast_le Fin.castLE_comp_castLE
 
-/-- `cast eq i` embeds `i` into an equal `Fin` type, see also `Equiv.finCongr`. -/
-def cast (eq : n = m) : Fin n ≃o Fin m where
+/-- `castIso eq i` embeds `i` into an equal `Fin` type, see also `Equiv.finCongr`. -/
+def castIso (eq : n = m) : Fin n ≃o Fin m where
   toEquiv := ⟨castLE eq.le, castLE eq.symm.le, fun _ => eq_of_veq rfl, fun _ => eq_of_veq rfl⟩
   map_rel_iff' := Iff.rfl
-#align fin.cast Fin.cast
+#align fin.cast Fin.castIso
 
 @[simp]
-theorem symm_cast (h : n = m) : (cast h).symm = cast h.symm := by simp
-#align fin.symm_cast Fin.symm_cast
+theorem symm_castIso (h : n = m) : (castIso h).symm = castIso h.symm := by simp
+#align fin.symm_cast Fin.symm_castIso
 
-theorem coe_cast (h : n = m) (i : Fin n) : (cast h i : ℕ) = i := by simp
-#align fin.coe_cast Fin.coe_cast
+theorem coe_castIso (h : n = m) (i : Fin n) : (castIso h i : ℕ) = i := by simp
+#align fin.coe_cast Fin.coe_castIso
 
 @[simp]
-theorem cast_zero {n' : ℕ} [NeZero n] {h : n = n'} : cast h (0 : Fin n) =
+theorem castIso_zero {n' : ℕ} [NeZero n] {h : n = n'} : castIso h (0 : Fin n) =
     by { haveI : NeZero n' := by {rw [← h]; infer_instance}; exact 0} :=
   ext rfl
-#align fin.cast_zero Fin.cast_zero
+#align fin.cast_zero Fin.castIso_zero
 
 @[simp]
-theorem cast_last {n' : ℕ} {h : n + 1 = n' + 1} : cast h (last n) = last n' :=
-  ext (by rw [coe_cast, val_last, val_last, Nat.succ_injective h])
-#align fin.cast_last Fin.cast_last
+theorem castIso_last {n' : ℕ} {h : n + 1 = n' + 1} : castIso h (last n) = last n' :=
+  ext (by rw [coe_castIso, val_last, val_last, Nat.succ_injective h])
+#align fin.cast_last Fin.castIso_last
 
 @[simp]
-theorem cast_mk (h : n = m) (i : ℕ) (hn : i < n) :
-    cast h ⟨i, hn⟩ = ⟨i, lt_of_lt_of_le hn h.le⟩ := by
+theorem castIso_mk (h : n = m) (i : ℕ) (hn : i < n) :
+    castIso h ⟨i, hn⟩ = ⟨i, lt_of_lt_of_le hn h.le⟩ := by
   ext
   simp
-#align fin.cast_mk Fin.cast_mk
+#align fin.cast_mk Fin.castIso_mk
 
 @[simp]
-theorem cast_trans {k : ℕ} (h : n = m) (h' : m = k) {i : Fin n} :
-    cast h' (cast h i) = cast (Eq.trans h h') i := by
+theorem castIso_trans {k : ℕ} (h : n = m) (h' : m = k) {i : Fin n} :
+    castIso h' (castIso h i) = castIso (Eq.trans h h') i := by
   ext
   simp
-#align fin.cast_trans Fin.cast_trans
+#align fin.cast_trans Fin.castIso_trans
 
 @[simp]
-theorem cast_refl (h : n = n := rfl) : cast h = OrderIso.refl (Fin n) := by
+theorem castIso_refl (h : n = n := rfl) : castIso h = OrderIso.refl (Fin n) := by
   ext
   simp
-#align fin.cast_refl Fin.cast_refl
+#align fin.cast_refl Fin.castIso_refl
 
 theorem castLE_of_eq {m n : ℕ} (h : m = n) {h' : m ≤ n} :
-    (castLE h' : Fin m → Fin n) = Fin.cast h :=
+    (castLE h' : Fin m → Fin n) = Fin.castIso h :=
   funext fun _ => by ext; simp
 #align fin.cast_le_of_eq Fin.castLE_of_eq
 
-/-- While in many cases `Fin.cast` is better than `Equiv.cast`/`cast`, sometimes we want to apply
+/-- While in many cases `Fin.castIso` is better than `Equiv.cast`/`cast`, sometimes we want to apply
 a generic theorem about `cast`. -/
-theorem cast_to_equiv (h : n = m) : (cast h).toEquiv = Equiv.cast (h ▸ rfl) := by
+theorem castIso_to_equiv (h : n = m) : (castIso h).toEquiv = Equiv.cast (h ▸ rfl) := by
   subst h
   simp
-#align fin.cast_to_equiv Fin.cast_to_equiv
+#align fin.cast_to_equiv Fin.castIso_to_equiv
 
-/-- While in many cases `Fin.cast` is better than `Equiv.cast`/`cast`, sometimes we want to apply
+/-- While in many cases `Fin.castIso` is better than `Equiv.cast`/`cast`, sometimes we want to apply
 a generic theorem about `cast`. -/
-theorem cast_eq_cast (h : n = m) : (cast h : Fin n → Fin m) = cast (h ▸ rfl) := by
+theorem castIso_eq_cast (h : n = m) : (castIso h : Fin n → Fin m) = cast (h ▸ rfl) := by
   subst h
   ext
   simp
-#align fin.cast_eq_cast Fin.cast_eq_cast
+#align fin.cast_eq_cast Fin.castIso_eq_cast
 
 /-- `castAdd m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAdd` and `Fin.addNat`. -/
 def castAdd (m) : Fin n ↪o Fin (n + m) :=
@@ -1132,9 +1132,9 @@ theorem coe_castAdd (m : ℕ) (i : Fin n) : (castAdd m i : ℕ) = i :=
 #align fin.coe_cast_add Fin.coe_castAdd
 
 @[simp]
-theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = cast rfl := by
+theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = castIso rfl := by
   ext
-  simp only [Nat.add_zero, cast_refl, OrderIso.refl_apply]
+  simp only [Nat.add_zero, castIso_refl, OrderIso.refl_apply]
   rfl
 #align fin.cast_add_zero Fin.castAdd_zero
 
@@ -1160,43 +1160,43 @@ theorem castLT_castAdd (m : ℕ) (i : Fin n) : castLT (castAdd m i) (castAdd_lt
   simp
 #align fin.cast_lt_cast_add Fin.castLT_castAdd
 
-/-- For rewriting in the reverse direction, see `Fin.cast_castAdd_left`. -/
-theorem castAdd_cast {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n) :
-    castAdd m (Fin.cast h i) = Fin.cast (congr_arg (. + m) h) (castAdd m i) :=
+/-- For rewriting in the reverse direction, see `Fin.castIso_castAdd_left`. -/
+theorem castAdd_castIso {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n) :
+    castAdd m (Fin.castIso h i) = Fin.castIso (congr_arg (. + m) h) (castAdd m i) :=
   ext rfl
-#align fin.cast_add_cast Fin.castAdd_cast
+#align fin.cast_add_cast Fin.castAdd_castIso
 
-theorem cast_castAdd_left {n n' m : ℕ} (i : Fin n') (h : n' + m = n + m) :
-    cast h (castAdd m i) = castAdd m (cast (add_right_cancel h) i) := by
+theorem castIso_castAdd_left {n n' m : ℕ} (i : Fin n') (h : n' + m = n + m) :
+    castIso h (castAdd m i) = castAdd m (castIso (add_right_cancel h) i) := by
   ext
   simp
-#align fin.cast_cast_add_left Fin.cast_castAdd_left
+#align fin.cast_cast_add_left Fin.castIso_castAdd_left
 
 @[simp]
-theorem cast_castAdd_right {n m m' : ℕ} (i : Fin n) (h : n + m' = n + m) :
-    cast h (castAdd m' i) = castAdd m i := by
+theorem castIso_castAdd_right {n m m' : ℕ} (i : Fin n) (h : n + m' = n + m) :
+    castIso h (castAdd m' i) = castAdd m i := by
   ext
   simp
-#align fin.cast_cast_add_right Fin.cast_castAdd_right
+#align fin.cast_cast_add_right Fin.castIso_castAdd_right
 
 theorem castAdd_castAdd {m n p : ℕ} (i : Fin m) :
-    castAdd p (castAdd n i) = cast (add_assoc _ _ _).symm (castAdd (n + p) i) := by
+    castAdd p (castAdd n i) = castIso (add_assoc _ _ _).symm (castAdd (n + p) i) := by
   ext
   simp
 #align fin.cast_add_cast_add Fin.castAdd_castAdd
 
-/-- The cast of the successor is the successor of the cast. See `Fin.succ_cast_eq` for rewriting in
-the reverse direction. -/
+/-- The cast of the successor is the successor of the cast.
+See `Fin.succ_castIso_eq` for rewriting in the reverse direction. -/
 @[simp]
-theorem cast_succ_eq {n' : ℕ} (i : Fin n) (h : n.succ = n'.succ) :
-    cast h i.succ = (cast (Nat.succ.inj h) i).succ :=
+theorem castIso_succ_eq {n' : ℕ} (i : Fin n) (h : n.succ = n'.succ) :
+    castIso h i.succ = (castIso (Nat.succ.inj h) i).succ :=
   ext <| by simp
-#align fin.cast_succ_eq Fin.cast_succ_eq
+#align fin.cast_succ_eq Fin.castIso_succ_eq
 
-theorem succ_cast_eq {n' : ℕ} (i : Fin n) (h : n = n') :
-    (cast h i).succ = cast (by rw [h]) i.succ :=
+theorem succ_castIso_eq {n' : ℕ} (i : Fin n) (h : n = n') :
+    (castIso h i).succ = castIso (by rw [h]) i.succ :=
   ext <| by simp
-#align fin.succ_cast_eq Fin.succ_cast_eq
+#align fin.succ_cast_eq Fin.succ_castIso_eq
 
 /-- `castSucc i` embeds `i : Fin n` in `Fin (n+1)`. -/
 def castSucc : Fin n ↪o Fin (n + 1) :=
@@ -1214,11 +1214,11 @@ theorem castSucc_mk (n i : ℕ) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt
 #align fin.cast_succ_mk Fin.castSucc_mk
 
 @[simp]
-theorem cast_castSucc {n' : ℕ} {h : n + 1 = n' + 1} {i : Fin n} :
-    cast h (castSucc i) = castSucc (cast (Nat.succ_injective h) i) := by
+theorem castIso_castSucc {n' : ℕ} {h : n + 1 = n' + 1} {i : Fin n} :
+    castIso h (castSucc i) = castSucc (castIso (Nat.succ_injective h) i) := by
   ext
-  simp only [coe_cast, coe_castSucc]
-#align fin.cast_cast_succ Fin.cast_castSucc
+  simp only [coe_castIso, coe_castSucc]
+#align fin.cast_cast_succ Fin.castIso_castSucc
 
 theorem castSucc_lt_succ (i : Fin n) : Fin.castSucc i < i.succ :=
   lt_iff_val_lt_val.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
@@ -1364,28 +1364,28 @@ theorem addNat_mk (n i : ℕ) (hi : i < m) : addNat n ⟨i, hi⟩ = ⟨i + n, ad
 #align fin.add_nat_mk Fin.addNat_mk
 
 @[simp]
-theorem cast_addNat_zero {n n' : ℕ} (i : Fin n) (h : n + 0 = n') :
-    cast h (addNat 0 i) = cast ((add_zero _).symm.trans h) i :=
+theorem castIso_addNat_zero {n n' : ℕ} (i : Fin n) (h : n + 0 = n') :
+    castIso h (addNat 0 i) = castIso ((add_zero _).symm.trans h) i :=
   ext <| add_zero _
-#align fin.cast_add_nat_zero Fin.cast_addNat_zero
+#align fin.cast_add_nat_zero Fin.castIso_addNat_zero
 
-/-- For rewriting in the reverse direction, see `Fin.cast_addNat_left`. -/
-theorem addNat_cast {n n' m : ℕ} (i : Fin n') (h : n' = n) :
-    addNat m (cast h i) = cast (congr_arg (. + m) h) (addNat m i) :=
+/-- For rewriting in the reverse direction, see `Fin.castIso_addNat_left`. -/
+theorem addNat_castIso {n n' m : ℕ} (i : Fin n') (h : n' = n) :
+    addNat m (castIso h i) = castIso (congr_arg (. + m) h) (addNat m i) :=
   ext rfl
-#align fin.add_nat_cast Fin.addNat_cast
+#align fin.add_nat_cast Fin.addNat_castIso
 
-theorem cast_addNat_left {n n' m : ℕ} (i : Fin n') (h : n' + m = n + m) :
-    cast h (addNat m i) = addNat m (cast (add_right_cancel h) i) := by
+theorem castIso_addNat_left {n n' m : ℕ} (i : Fin n') (h : n' + m = n + m) :
+    castIso h (addNat m i) = addNat m (castIso (add_right_cancel h) i) := by
   ext
   simp
-#align fin.cast_add_nat_left Fin.cast_addNat_left
+#align fin.cast_add_nat_left Fin.castIso_addNat_left
 
 @[simp]
-theorem cast_addNat_right {n m m' : ℕ} (i : Fin n) (h : n + m' = n + m) :
-    cast h (addNat m' i) = addNat m i :=
+theorem castIso_addNat_right {n m m' : ℕ} (i : Fin n) (h : n + m' = n + m) :
+    castIso h (addNat m' i) = addNat m i :=
   ext <| (congr_arg ((· + ·) (i : ℕ)) (add_left_cancel h) : _)
-#align fin.cast_add_nat_right Fin.cast_addNat_right
+#align fin.cast_add_nat_right Fin.castIso_addNat_right
 
 /-- `natAdd n i` adds `n` to `i` "on the left". -/
 def natAdd (n) {m} : Fin m ↪o Fin (n + m) :=
@@ -1407,62 +1407,64 @@ theorem le_coe_natAdd (m : ℕ) (i : Fin n) : m ≤ natAdd m i :=
   Nat.le_add_right _ _
 #align fin.le_coe_nat_add Fin.le_coe_natAdd
 
-theorem natAdd_zero {n : ℕ} : Fin.natAdd 0 = (Fin.cast (zero_add n).symm).toRelEmbedding := by
+theorem natAdd_zero {n : ℕ} : Fin.natAdd 0 = (Fin.castIso (zero_add n).symm).toRelEmbedding := by
   ext
   simp
 #align fin.nat_add_zero Fin.natAdd_zero
 
-/-- For rewriting in the reverse direction, see `Fin.cast_natAdd_right`. -/
-theorem natAdd_cast {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n) :
-    natAdd m (cast h i) = cast (congr_arg _ h) (natAdd m i) := by
+/-- For rewriting in the reverse direction, see `Fin.castIso_natAdd_right`. -/
+theorem natAdd_castIso {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n) :
+    natAdd m (castIso h i) = castIso (congr_arg _ h) (natAdd m i) := by
   ext
   simp
-#align fin.nat_add_cast Fin.natAdd_cast
+#align fin.nat_add_cast Fin.natAdd_castIso
 
-theorem cast_natAdd_right {n n' m : ℕ} (i : Fin n') (h : m + n' = m + n) :
-    cast h (natAdd m i) = natAdd m (cast (add_left_cancel h) i) := by
+theorem castIso_natAdd_right {n n' m : ℕ} (i : Fin n') (h : m + n' = m + n) :
+    castIso h (natAdd m i) = natAdd m (castIso (add_left_cancel h) i) := by
   ext
   simp
-#align fin.cast_nat_add_right Fin.cast_natAdd_right
+#align fin.cast_nat_add_right Fin.castIso_natAdd_right
 
 @[simp]
-theorem cast_natAdd_left {n m m' : ℕ} (i : Fin n) (h : m' + n = m + n) :
-    cast h (natAdd m' i) = natAdd m i :=
+theorem castIso_natAdd_left {n m m' : ℕ} (i : Fin n) (h : m' + n = m + n) :
+    castIso h (natAdd m' i) = natAdd m i :=
   ext <| (congr_arg (· + (i : ℕ)) (add_right_cancel h) : _)
-#align fin.cast_nat_add_left Fin.cast_natAdd_left
+#align fin.cast_nat_add_left Fin.castIso_natAdd_left
 
 theorem castAdd_natAdd (p m : ℕ) {n : ℕ} (i : Fin n) :
-    castAdd p (natAdd m i) = cast (add_assoc _ _ _).symm (natAdd m (castAdd p i)) := by
+    castAdd p (natAdd m i) = castIso (add_assoc _ _ _).symm (natAdd m (castAdd p i)) := by
   ext
   simp
 #align fin.cast_add_nat_add Fin.castAdd_natAdd
 
 theorem natAdd_castAdd (p m : ℕ) {n : ℕ} (i : Fin n) :
-    natAdd m (castAdd p i) = cast (add_assoc _ _ _) (castAdd p (natAdd m i)) := by
+    natAdd m (castAdd p i) = castIso (add_assoc _ _ _) (castAdd p (natAdd m i)) := by
   ext
   simp
 #align fin.nat_add_cast_add Fin.natAdd_castAdd
 
 theorem natAdd_natAdd (m n : ℕ) {p : ℕ} (i : Fin p) :
-    natAdd m (natAdd n i) = cast (add_assoc _ _ _) (natAdd (m + n) i) :=
+    natAdd m (natAdd n i) = castIso (add_assoc _ _ _) (natAdd (m + n) i) :=
   ext <| (add_assoc _ _ _).symm
 #align fin.nat_add_nat_add Fin.natAdd_natAdd
 
 @[simp]
-theorem cast_natAdd_zero {n n' : ℕ} (i : Fin n) (h : 0 + n = n') :
-    cast h (natAdd 0 i) = cast ((zero_add _).symm.trans h) i :=
+theorem castIso_natAdd_zero {n n' : ℕ} (i : Fin n) (h : 0 + n = n') :
+    castIso h (natAdd 0 i) = castIso ((zero_add _).symm.trans h) i :=
   ext <| zero_add _
-#align fin.cast_nat_add_zero Fin.cast_natAdd_zero
+#align fin.cast_nat_add_zero Fin.castIso_natAdd_zero
 
 @[simp]
-theorem cast_natAdd (n : ℕ) {m : ℕ} (i : Fin m) : cast (add_comm _ _) (natAdd n i) = addNat n i :=
+theorem castIso_natAdd (n : ℕ) {m : ℕ} (i : Fin m) :
+    castIso (add_comm _ _) (natAdd n i) = addNat n i :=
   ext <| add_comm _ _
-#align fin.cast_nat_add Fin.cast_natAdd
+#align fin.cast_nat_add Fin.castIso_natAdd
 
 @[simp]
-theorem cast_addNat {n : ℕ} (m : ℕ) (i : Fin n) : cast (add_comm _ _) (addNat m i) = natAdd m i :=
+theorem castIso_addNat {n : ℕ} (m : ℕ) (i : Fin n) :
+    castIso (add_comm _ _) (addNat m i) = natAdd m i :=
   ext <| add_comm _ _
-#align fin.cast_add_nat Fin.cast_addNat
+#align fin.cast_add_nat Fin.castIso_addNat
 
 @[simp]
 theorem natAdd_last {m n : ℕ} : natAdd n (last m) = last (n + m) :=
@@ -1604,9 +1606,9 @@ theorem subNat_addNat (i : Fin n) (m : ℕ) (h : m ≤ addNat m i := le_coe_addN
 #align fin.sub_nat_add_nat Fin.subNat_addNat
 
 @[simp]
-theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
-    natAdd n (subNat n (cast (add_comm _ _) i) h) = i := by simp [← cast_addNat]
-#align fin.nat_add_sub_nat_cast Fin.natAdd_subNat_cast
+theorem natAdd_subNat_castIso {i : Fin (n + m)} (h : n ≤ i) :
+    natAdd n (subNat n (castIso (add_comm _ _) i) h) = i := by simp [← castIso_addNat]
+#align fin.nat_add_sub_nat_cast Fin.natAdd_subNat_castIso
 
 end Pred
 
@@ -1841,7 +1843,7 @@ theorem lastCases_castSucc {n : ℕ} {C : Fin (n + 1) → Sort _} (hlast : C (Fi
 def addCases {m n : ℕ} {C : Fin (m + n) → Sort u} (hleft : ∀ i, C (castAdd n i))
     (hright : ∀ i, C (natAdd m i)) (i : Fin (m + n)) : C i :=
   if hi : (i : ℕ) < m then (castAdd_castLT n i hi) ▸ (hleft (castLT i hi))
-  else (natAdd_subNat_cast (le_of_not_lt hi)) ▸ (hright _)
+  else (natAdd_subNat_castIso (le_of_not_lt hi)) ▸ (hright _)
 #align fin.add_cases Fin.addCases
 
 @[simp]
diff --git a/Mathlib/Data/Fin/Tuple/Basic.lean b/Mathlib/Data/Fin/Tuple/Basic.lean
index da3366112c660..802167cfa56d2 100644
--- a/Mathlib/Data/Fin/Tuple/Basic.lean
+++ b/Mathlib/Data/Fin/Tuple/Basic.lean
@@ -305,24 +305,24 @@ theorem append_right {α : Type _} (u : Fin m → α) (v : Fin n → α) (i : Fi
 #align fin.append_right Fin.append_right
 
 theorem append_right_nil {α : Type _} (u : Fin m → α) (v : Fin n → α) (hv : n = 0) :
-    append u v = u ∘ Fin.cast (by rw [hv, add_zero]) := by
+    append u v = u ∘ Fin.castIso (by rw [hv, add_zero]) := by
   refine' funext (Fin.addCases (fun l => _) fun r => _)
   · rw [append_left, Function.comp_apply]
     refine' congr_arg u (Fin.ext _)
     simp
-  · exact (Fin.cast hv r).elim0'
+  · exact (Fin.castIso hv r).elim0'
 #align fin.append_right_nil Fin.append_right_nil
 
 @[simp]
 theorem append_elim0' {α : Type _} (u : Fin m → α) :
-    append u Fin.elim0' = u ∘ Fin.cast (add_zero _) :=
+    append u Fin.elim0' = u ∘ Fin.castIso (add_zero _) :=
   append_right_nil _ _ rfl
 #align fin.append_elim0' Fin.append_elim0'
 
 theorem append_left_nil {α : Type _} (u : Fin m → α) (v : Fin n → α) (hu : m = 0) :
-    append u v = v ∘ Fin.cast (by rw [hu, zero_add]) := by
+    append u v = v ∘ Fin.castIso (by rw [hu, zero_add]) := by
   refine' funext (Fin.addCases (fun l => _) fun r => _)
-  · exact (Fin.cast hu l).elim0'
+  · exact (Fin.castIso hu l).elim0'
   · rw [append_right, Function.comp_apply]
     refine' congr_arg v (Fin.ext _)
     simp [hu]
@@ -330,12 +330,12 @@ theorem append_left_nil {α : Type _} (u : Fin m → α) (v : Fin n → α) (hu
 
 @[simp]
 theorem elim0'_append {α : Type _} (v : Fin n → α) :
-    append Fin.elim0' v = v ∘ Fin.cast (zero_add _) :=
+    append Fin.elim0' v = v ∘ Fin.castIso (zero_add _) :=
   append_left_nil _ _ rfl
 #align fin.elim0'_append Fin.elim0'_append
 
 theorem append_assoc {p : ℕ} {α : Type _} (a : Fin m → α) (b : Fin n → α) (c : Fin p → α) :
-    append (append a b) c = append a (append b c) ∘ Fin.cast (add_assoc _ _ _) := by
+    append (append a b) c = append a (append b c) ∘ Fin.castIso (add_assoc _ _ _) := by
   ext i
   rw [Function.comp_apply]
   refine' Fin.addCases (fun l => _) (fun r => _) i
@@ -351,14 +351,14 @@ theorem append_assoc {p : ℕ} {α : Type _} (a : Fin m → α) (b : Fin n → 
 
 /-- Appending a one-tuple to the left is the same as `Fin.cons`. -/
 theorem append_left_eq_cons {α : Type _} {n : ℕ} (x₀ : Fin 1 → α) (x : Fin n → α) :
-    Fin.append x₀ x = Fin.cons (x₀ 0) x ∘ Fin.cast (add_comm _ _) := by
+    Fin.append x₀ x = Fin.cons (x₀ 0) x ∘ Fin.castIso (add_comm _ _) := by
   ext i
   refine' Fin.addCases _ _ i <;> clear i
   · intro i
     rw [Subsingleton.elim i 0, Fin.append_left, Function.comp_apply, eq_comm]
     exact Fin.cons_zero _ _
   · intro i
-    rw [Fin.append_right, Function.comp_apply, Fin.cast_natAdd, eq_comm, Fin.addNat_one]
+    rw [Fin.append_right, Function.comp_apply, Fin.castIso_natAdd, eq_comm, Fin.addNat_one]
     exact Fin.cons_succ _ _ _
 #align fin.append_left_eq_cons Fin.append_left_eq_cons
 
@@ -380,36 +380,36 @@ theorem repeat_apply {α : Type _} (a : Fin n → α) (i : Fin (m * n)) :
 
 @[simp]
 theorem repeat_zero {α : Type _} (a : Fin n → α) :
-    Fin.repeat 0 a = Fin.elim0' ∘ cast (zero_mul _) :=
-  funext fun x => (cast (zero_mul _) x).elim0'
+    Fin.repeat 0 a = Fin.elim0' ∘ castIso (zero_mul _) :=
+  funext fun x => (castIso (zero_mul _) x).elim0'
 #align fin.repeat_zero Fin.repeat_zero
 
 @[simp]
-theorem repeat_one {α : Type _} (a : Fin n → α) : Fin.repeat 1 a = a ∘ cast (one_mul _) := by
+theorem repeat_one {α : Type _} (a : Fin n → α) : Fin.repeat 1 a = a ∘ castIso (one_mul _) := by
   generalize_proofs h
   apply funext
-  rw [(Fin.cast h.symm).surjective.forall]
+  rw [(Fin.castIso h.symm).surjective.forall]
   intro i
   simp [modNat, Nat.mod_eq_of_lt i.is_lt]
 #align fin.repeat_one Fin.repeat_one
 
 theorem repeat_succ {α : Type _} (a : Fin n → α) (m : ℕ) :
     Fin.repeat m.succ a =
-      append a (Fin.repeat m a) ∘ cast ((Nat.succ_mul _ _).trans (add_comm _ _)) := by
+      append a (Fin.repeat m a) ∘ castIso ((Nat.succ_mul _ _).trans (add_comm _ _)) := by
   generalize_proofs h
   apply funext
-  rw [(Fin.cast h.symm).surjective.forall]
+  rw [(Fin.castIso h.symm).surjective.forall]
   refine' Fin.addCases (fun l => _) fun r => _
   · simp [modNat, Nat.mod_eq_of_lt l.is_lt]
   · simp [modNat]
 #align fin.repeat_succ Fin.repeat_succ
 
 @[simp]
-theorem repeat_add {α : Type _} (a : Fin n → α) (m₁ m₂ : ℕ) :
-    Fin.repeat (m₁ + m₂) a = append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ cast (add_mul _ _ _) := by
+theorem repeat_add {α : Type _} (a : Fin n → α) (m₁ m₂ : ℕ) : Fin.repeat (m₁ + m₂) a =
+    append (Fin.repeat m₁ a) (Fin.repeat m₂ a) ∘ castIso (add_mul _ _ _) := by
   generalize_proofs h
   apply funext
-  rw [(Fin.cast h.symm).surjective.forall]
+  rw [(Fin.castIso h.symm).surjective.forall]
   refine' Fin.addCases (fun l => _) fun r => _
   · simp [modNat, Nat.mod_eq_of_lt l.is_lt]
   · simp [modNat, Nat.add_mod]
@@ -988,20 +988,20 @@ theorem contractNth_apply_of_ne (j : Fin (n + 1)) (op : α → α → α) (g : F
 end ContractNth
 
 /-- To show two sigma pairs of tuples agree, it to show the second elements are related via
-`Fin.cast`. -/
-theorem sigma_eq_of_eq_comp_cast {α : Type _} :
-    ∀ {a b : Σii, Fin ii → α} (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h → a = b
+`Fin.castIso`. -/
+theorem sigma_eq_of_eq_comp_castIso {α : Type _} :
+    ∀ {a b : Σii, Fin ii → α} (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.castIso h → a = b
   | ⟨ai, a⟩, ⟨bi, b⟩, hi, h => by
     dsimp only at hi
     subst hi
     simpa using h
-#align fin.sigma_eq_of_eq_comp_cast Fin.sigma_eq_of_eq_comp_cast
+#align fin.sigma_eq_of_eq_comp_cast Fin.sigma_eq_of_eq_comp_castIso
 
-/-- `Fin.sigma_eq_of_eq_comp_cast` as an `iff`. -/
-theorem sigma_eq_iff_eq_comp_cast {α : Type _} {a b : Σii, Fin ii → α} :
-    a = b ↔ ∃ h : a.fst = b.fst, a.snd = b.snd ∘ Fin.cast h :=
+/-- `Fin.sigma_eq_of_eq_comp_castIso` as an `iff`. -/
+theorem sigma_eq_iff_eq_comp_castIso {α : Type _} {a b : Σii, Fin ii → α} :
+    a = b ↔ ∃ h : a.fst = b.fst, a.snd = b.snd ∘ Fin.castIso h :=
   ⟨fun h ↦ h ▸ ⟨rfl, funext <| Fin.rec fun _ _ ↦ rfl⟩, fun ⟨_, h'⟩ ↦
-    sigma_eq_of_eq_comp_cast _ h'⟩
-#align fin.sigma_eq_iff_eq_comp_cast Fin.sigma_eq_iff_eq_comp_cast
+    sigma_eq_of_eq_comp_castIso _ h'⟩
+#align fin.sigma_eq_iff_eq_comp_cast Fin.sigma_eq_iff_eq_comp_castIso
 
 end Fin
diff --git a/Mathlib/Data/Fin/VecNotation.lean b/Mathlib/Data/Fin/VecNotation.lean
index 58f2aaed70779..9d2e6a828fb4b 100644
--- a/Mathlib/Data/Fin/VecNotation.lean
+++ b/Mathlib/Data/Fin/VecNotation.lean
@@ -259,7 +259,7 @@ This turns out to be helpful when providing simp lemmas to reduce `![a, b, c] n`
 that `vecAppend ho u v 0` is valid. `Fin.append u v 0` is not valid in this case because there is
 no `Zero (Fin (m + n))` instance. -/
 def vecAppend {α : Type _} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) : Fin o → α :=
-  Fin.append u v ∘ Fin.cast ho
+  Fin.append u v ∘ Fin.castIso ho
 #align matrix.vec_append Matrix.vecAppend
 
 theorem vecAppend_eq_ite {α : Type _} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α) :
diff --git a/Mathlib/Data/Finset/Sort.lean b/Mathlib/Data/Finset/Sort.lean
index 5da530721ffc7..3beea6df0bc02 100644
--- a/Mathlib/Data/Finset/Sort.lean
+++ b/Mathlib/Data/Finset/Sort.lean
@@ -147,7 +147,7 @@ is the increasing bijection between `Fin k` and `s` as an `OrderIso`. Here, `h`
 the cardinality of `s` is `k`. We use this instead of an iso `Fin s.card ≃o s` to avoid
 casting issues in further uses of this function. -/
 def orderIsoOfFin (s : Finset α) {k : ℕ} (h : s.card = k) : Fin k ≃o s :=
-  OrderIso.trans (Fin.cast ((length_sort (α := α) (· ≤ ·)).trans h).symm) <|
+  OrderIso.trans (Fin.castIso ((length_sort (α := α) (· ≤ ·)).trans h).symm) <|
     (s.sort_sorted_lt.getIso _).trans <| OrderIso.setCongr _ _ <| Set.ext fun _ => mem_sort _
 #align finset.order_iso_of_fin Finset.orderIsoOfFin
 
diff --git a/Mathlib/Data/Fintype/Card.lean b/Mathlib/Data/Fintype/Card.lean
index 72725fcccc1ca..8e73b8f958eb0 100644
--- a/Mathlib/Data/Fintype/Card.lean
+++ b/Mathlib/Data/Fintype/Card.lean
@@ -168,7 +168,7 @@ See `Fintype.equivFinOfCardEq` for the noncomputable definition,
 and `Fintype.truncEquivFin` and `Fintype.equivFin` for the bijection `α ≃ Fin (card α)`.
 -/
 def truncEquivFinOfCardEq [DecidableEq α] {n : ℕ} (h : Fintype.card α = n) : Trunc (α ≃ Fin n) :=
-  (truncEquivFin α).map fun e => e.trans (Fin.cast h).toEquiv
+  (truncEquivFin α).map fun e => e.trans (Fin.castIso h).toEquiv
 #align fintype.trunc_equiv_fin_of_card_eq Fintype.truncEquivFinOfCardEq
 
 /-- If the cardinality of `α` is `n`, there is noncomputably a bijection between `α` and `Fin n`.
@@ -315,7 +315,7 @@ theorem fin_injective : Function.Injective Fin := fun m n h =>
 
 /-- A reversed version of `Fin.cast_eq_cast` that is easier to rewrite with. -/
 theorem Fin.cast_eq_cast' {n m : ℕ} (h : Fin n = Fin m) :
-    _root_.cast h = ⇑(Fin.cast <| fin_injective h) := by
+    _root_.cast h = ⇑(Fin.castIso <| fin_injective h) := by
   cases fin_injective h
   rfl
 #align fin.cast_eq_cast' Fin.cast_eq_cast'
diff --git a/Mathlib/Data/List/OfFn.lean b/Mathlib/Data/List/OfFn.lean
index 3721ec96d8ef0..1540c5f773a93 100644
--- a/Mathlib/Data/List/OfFn.lean
+++ b/Mathlib/Data/List/OfFn.lean
@@ -49,11 +49,11 @@ theorem length_ofFn {n} (f : Fin n → α) : length (ofFn f) = n := by
 
 --Porting note: new theorem
 @[simp]
-theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f (Fin.cast (by simp) i) := by
+theorem get_ofFn {n} (f : Fin n → α) (i) : get (ofFn f) i = f (Fin.castIso (by simp) i) := by
   have := Array.getElem_ofFn f i (by simpa using i.2)
   cases' i with i hi
   simp only [getElem, Array.get] at this
-  simp only [Fin.cast_mk]
+  simp only [Fin.castIso_mk]
   rw [← this]
   congr <;> simp [ofFn]
 
@@ -102,9 +102,9 @@ theorem map_ofFn {β : Type _} {n : ℕ} (f : Fin n → α) (g : α → β) :
 
 @[congr]
 theorem ofFn_congr {m n : ℕ} (h : m = n) (f : Fin m → α) :
-    ofFn f = ofFn fun i : Fin n => f (Fin.cast h.symm i) := by
+    ofFn f = ofFn fun i : Fin n => f (Fin.castIso h.symm i) := by
   subst h
-  simp_rw [Fin.cast_refl, OrderIso.refl_apply]
+  simp_rw [Fin.castIso_refl, OrderIso.refl_apply]
 #align list.of_fn_congr List.ofFn_congr
 
 /-- `ofFn` on an empty domain is the empty list. -/
@@ -151,7 +151,7 @@ theorem ofFn_add {m n} (f : Fin (m + n) → α) :
     List.ofFn f =
       (List.ofFn fun i => f (Fin.castAdd n i)) ++ List.ofFn fun j => f (Fin.natAdd m j) := by
   induction' n with n IH
-  · rw [ofFn_zero, append_nil, Fin.castAdd_zero, Fin.cast_refl]
+  · rw [ofFn_zero, append_nil, Fin.castAdd_zero, Fin.castIso_refl]
     rfl
   · rw [ofFn_succ', ofFn_succ', IH, append_concat]
     rfl
@@ -181,7 +181,7 @@ theorem ofFn_mul' {m n} (f : Fin (m * n) → α) :
     calc
       m * i + j < m * (i + 1) := (add_lt_add_left j.prop _).trans_eq (mul_add_one (_ : ℕ) _).symm
       _ ≤ _ := Nat.mul_le_mul_left _ i.prop⟩) := by
-  simp_rw [mul_comm m n, mul_comm m, ofFn_mul, Fin.cast_mk]
+  simp_rw [mul_comm m n, mul_comm m, ofFn_mul, Fin.castIso_mk]
 #align list.of_fn_mul' List.ofFn_mul'
 
 theorem ofFn_get : ∀ l : List α, (ofFn (get l)) = l
@@ -202,7 +202,7 @@ theorem ofFn_nthLe : ∀ l : List α, (ofFn fun i => nthLe l i i.2) = l :=
 -- is much more useful
 theorem mem_ofFn {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f := by
   simp only [mem_iff_get, Set.mem_range, get_ofFn]
-  exact ⟨fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩⟩
+  exact ⟨fun ⟨i, hi⟩ => ⟨Fin.castIso (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.castIso (by simp) i, hi⟩⟩
 #align list.mem_of_fn List.mem_ofFn
 
 @[simp]
@@ -226,7 +226,7 @@ theorem ofFn_fin_repeat {m} (a : Fin m → α) (n : ℕ) :
 @[simp]
 theorem pairwise_ofFn {R : α → α → Prop} {n} {f : Fin n → α} :
     (ofFn f).Pairwise R ↔ ∀ ⦃i j⦄, i < j → R (f i) (f j) := by
-  simp only [pairwise_iff_get, (Fin.cast (length_ofFn f)).surjective.forall, get_ofFn,
+  simp only [pairwise_iff_get, (Fin.castIso (length_ofFn f)).surjective.forall, get_ofFn,
     OrderIso.lt_iff_lt]
 #align list.pairwise_of_fn List.pairwise_ofFn
 
@@ -237,7 +237,7 @@ def equivSigmaTuple : List α ≃ Σn, Fin n → α where
   invFun f := List.ofFn f.2
   left_inv := List.ofFn_get
   right_inv := fun ⟨_, f⟩ =>
-    Fin.sigma_eq_of_eq_comp_cast (length_ofFn _) <| funext fun i => get_ofFn f i
+    Fin.sigma_eq_of_eq_comp_castIso (length_ofFn _) <| funext fun i => get_ofFn f i
 #align list.equiv_sigma_tuple List.equivSigmaTuple
 #align list.equiv_sigma_tuple_symm_apply List.equivSigmaTuple_symm_apply
 #align list.equiv_sigma_tuple_apply_fst List.equivSigmaTuple_apply_fst
diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean
index 78fead05eca8a..fb44caaa48605 100644
--- a/Mathlib/Data/List/Sort.lean
+++ b/Mathlib/Data/List/Sort.lean
@@ -146,7 +146,7 @@ variable {n : ℕ} {α : Type uu} [Preorder α] {f : Fin n → α}
 
 theorem sorted_ofFn_iff {r : α → α → Prop} : (ofFn f).Sorted r ↔ ((· < ·) ⇒ r) f f := by
   simp_rw [Sorted, pairwise_iff_get, get_ofFn, Relator.LiftFun]
-  exact Iff.symm (Fin.cast _).surjective.forall₂
+  exact Iff.symm (Fin.castIso _).surjective.forall₂
 
 /-- The list `List.ofFn f` is strictly sorted with respect to `(· ≤ ·)` if and only if `f` is
 strictly monotone. -/
diff --git a/Mathlib/Data/Vector/Basic.lean b/Mathlib/Data/Vector/Basic.lean
index 8806d69a8321e..3d1bfc0b24470 100644
--- a/Mathlib/Data/Vector/Basic.lean
+++ b/Mathlib/Data/Vector/Basic.lean
@@ -115,7 +115,7 @@ theorem tail_map {β : Type _} (v : Vector α (n + 1)) (f : α → β) :
 #align vector.tail_map Vector.tail_map
 
 theorem get_eq_get (v : Vector α n) (i : Fin n) :
-    v.get i = v.toList.get (Fin.cast v.toList_length.symm i) :=
+    v.get i = v.toList.get (Fin.castIso v.toList_length.symm i) :=
   rfl
 #align vector.nth_eq_nth_le Vector.get_eq_get
 
diff --git a/Mathlib/Data/ZMod/Basic.lean b/Mathlib/Data/ZMod/Basic.lean
index 6eeb68c1dce0a..9ecfbe90b8a03 100644
--- a/Mathlib/Data/ZMod/Basic.lean
+++ b/Mathlib/Data/ZMod/Basic.lean
@@ -440,15 +440,15 @@ def ringEquivCongr {m n : ℕ} (h : m = n) : ZMod m ≃+* ZMod n := by
   · exfalso
     exact m.succ_ne_zero h
   · exact
-      { Fin.cast h with
+      { Fin.castIso h with
         map_mul' := fun a b => by
           dsimp [ZMod]
           ext
-          rw [Fin.coe_cast, Fin.coe_mul, Fin.coe_mul, Fin.coe_cast, Fin.coe_cast, ← h]
+          rw [Fin.coe_castIso, Fin.coe_mul, Fin.coe_mul, Fin.coe_castIso, Fin.coe_castIso, ← h]
         map_add' := fun a b => by
           dsimp [ZMod]
           ext
-          rw [Fin.coe_cast, Fin.val_add, Fin.val_add, Fin.coe_cast, Fin.coe_cast, ← h] }
+          rw [Fin.coe_castIso, Fin.val_add, Fin.val_add, Fin.coe_castIso, Fin.coe_castIso, ← h] }
 #align zmod.ring_equiv_congr ZMod.ringEquivCongr
 
 end CharEq
diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
index 1f3839aaf1d7f..391685e90e2e8 100644
--- a/Mathlib/GroupTheory/OrderOfElement.lean
+++ b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -763,7 +763,7 @@ theorem finEquivPowers_symm_apply [Finite G] (x : G) (n : ℕ) {hn : ∃ m : ℕ
   mapping `i • a` to `i • b`."]
 noncomputable def powersEquivPowers [Finite G] (h : orderOf x = orderOf y) :
     (Submonoid.powers x : Set G) ≃ (Submonoid.powers y : Set G) :=
-  (finEquivPowers x).symm.trans ((Fin.cast h).toEquiv.trans (finEquivPowers y))
+  (finEquivPowers x).symm.trans ((Fin.castIso h).toEquiv.trans (finEquivPowers y))
 #align powers_equiv_powers powersEquivPowers
 #align multiples_equiv_multiples multiplesEquivMultiples
 
@@ -869,7 +869,7 @@ theorem finEquivZpowers_symm_apply [Finite G] (x : G) (n : ℕ) {hn : ∃ m : 
   mapping `i • a` to `i • b`."]
 noncomputable def zpowersEquivZpowers [Finite G] (h : orderOf x = orderOf y) :
     (Subgroup.zpowers x : Set G) ≃ (Subgroup.zpowers y : Set G) :=
-  (finEquivZpowers x).symm.trans ((Fin.cast h).toEquiv.trans (finEquivZpowers y))
+  (finEquivZpowers x).symm.trans ((Fin.castIso h).toEquiv.trans (finEquivZpowers y))
 #align zpowers_equiv_zpowers zpowersEquivZpowers
 #align zmultiples_equiv_zmultiples zmultiplesEquivZmultiples
 
diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean
index 79b0a574528ac..29cd12f162f54 100644
--- a/Mathlib/LinearAlgebra/FiniteDimensional.lean
+++ b/Mathlib/LinearAlgebra/FiniteDimensional.lean
@@ -254,7 +254,7 @@ noncomputable def finBasis [FiniteDimensional K V] : Basis (Fin (finrank K V)) K
 /-- An `n`-dimensional vector space has a basis indexed by `Fin n`. -/
 noncomputable def finBasisOfFinrankEq [FiniteDimensional K V] {n : ℕ} (hn : finrank K V = n) :
     Basis (Fin n) K V :=
-  (finBasis K V).reindex (Fin.cast hn).toEquiv
+  (finBasis K V).reindex (Fin.castIso hn).toEquiv
 #align finite_dimensional.fin_basis_of_finrank_eq FiniteDimensional.finBasisOfFinrankEq
 
 variable {K V}
diff --git a/Mathlib/LinearAlgebra/TensorPower.lean b/Mathlib/LinearAlgebra/TensorPower.lean
index c4b7f20a7fb3a..4de95a93aa333 100644
--- a/Mathlib/LinearAlgebra/TensorPower.lean
+++ b/Mathlib/LinearAlgebra/TensorPower.lean
@@ -106,17 +106,17 @@ variable (R M)
 
 /-- Cast between "equal" tensor powers. -/
 def cast {i j} (h : i = j) : (⨂[R]^i) M ≃ₗ[R] (⨂[R]^j) M :=
-  reindex R M (Fin.cast h).toEquiv
+  reindex R M (Fin.castIso h).toEquiv
 #align tensor_power.cast TensorPower.cast
 
 theorem cast_tprod {i j} (h : i = j) (a : Fin i → M) :
-    cast R M h (tprod R a) = tprod R (a ∘ Fin.cast h.symm) :=
+    cast R M h (tprod R a) = tprod R (a ∘ Fin.castIso h.symm) :=
   reindex_tprod _ _
 #align tensor_power.cast_tprod TensorPower.cast_tprod
 
 @[simp]
 theorem cast_refl {i} (h : i = i) : cast R M h = LinearEquiv.refl _ _ :=
-  ((congr_arg fun f => reindex R M (RelIso.toEquiv f)) <| Fin.cast_refl h).trans reindex_refl
+  ((congr_arg fun f => reindex R M (RelIso.toEquiv f)) <| Fin.castIso_refl h).trans reindex_refl
 #align tensor_power.cast_refl TensorPower.cast_refl
 
 @[simp]
@@ -143,10 +143,10 @@ theorem gradedMonoid_eq_of_cast {a b : GradedMonoid fun n => ⨂[R] _ : Fin n, M
     (h2 : cast R M h a.snd = b.snd) : a = b := by
   refine' gradedMonoid_eq_of_reindex_cast h _
   rw [cast] at h2
-  rw [← Fin.cast_to_equiv, ← h2]
+  rw [← Fin.castIso_to_equiv, ← h2]
 #align tensor_power.graded_monoid_eq_of_cast TensorPower.gradedMonoid_eq_of_cast
 
--- named to match `Fin.cast_eq_cast`
+-- named to match `Fin.cast_eq_cast`, which is now `Fin.castIso_eq_cast`
 theorem cast_eq_cast {i j} (h : i = j) :
     ⇑(cast R M h) = _root_.cast (congrArg (fun i => (⨂[R]^i) M) h) := by
   subst h
@@ -216,7 +216,7 @@ theorem mul_assoc {na nb nc} (a : (⨂[R]^na) M) (b : (⨂[R]^nb) M) (c : (⨂[R
   congr with j
   rw [Fin.append_assoc]
   refine' congr_arg (Fin.append a (Fin.append b c)) (Fin.ext _)
-  rw [Fin.coe_cast, Fin.coe_cast]
+  rw [Fin.coe_castIso, Fin.coe_castIso]
 #align tensor_power.mul_assoc TensorPower.mul_assoc
 
 -- for now we just use the default for the `gnpow` field as it's easier.
diff --git a/Mathlib/Logic/Equiv/Fin.lean b/Mathlib/Logic/Equiv/Fin.lean
index 45b25efd73bfe..c9d6aaf095c99 100644
--- a/Mathlib/Logic/Equiv/Fin.lean
+++ b/Mathlib/Logic/Equiv/Fin.lean
@@ -106,7 +106,7 @@ def OrderIso.finTwoArrowIso (α : Type _) [Preorder α] : (Fin 2 → α) ≃o α
 
 /-- The 'identity' equivalence between `Fin n` and `Fin m` when `n = m`. -/
 def finCongr (h : m = n) : Fin m ≃ Fin n :=
-  (Fin.cast h).toEquiv
+  (Fin.castIso h).toEquiv
 #align fin_congr finCongr
 
 @[simp] theorem finCongr_apply_mk (h : m = n) (k : ℕ) (w : k < m) :
diff --git a/Mathlib/ModelTheory/Definability.lean b/Mathlib/ModelTheory/Definability.lean
index f5bde2398e01b..1accb2133211d 100644
--- a/Mathlib/ModelTheory/Definability.lean
+++ b/Mathlib/ModelTheory/Definability.lean
@@ -178,7 +178,7 @@ theorem Definable.image_comp_sum_inl_fin (m : ℕ) {s : Set (Sum α (Fin m) →
   refine' ⟨(BoundedFormula.relabel id φ).exs, _⟩
   ext x
   simp only [Set.mem_image, mem_setOf_eq, BoundedFormula.realize_exs,
-    BoundedFormula.realize_relabel, Function.comp.right_id, Fin.castAdd_zero, Fin.cast_refl]
+    BoundedFormula.realize_relabel, Function.comp.right_id, Fin.castAdd_zero, Fin.castIso_refl]
   constructor
   · rintro ⟨y, hy, rfl⟩
     exact
diff --git a/Mathlib/ModelTheory/Semantics.lean b/Mathlib/ModelTheory/Semantics.lean
index e7aeb68672b1c..3fa29275e1bb8 100644
--- a/Mathlib/ModelTheory/Semantics.lean
+++ b/Mathlib/ModelTheory/Semantics.lean
@@ -356,9 +356,9 @@ theorem realize_iff : (φ.iff ψ).Realize v xs ↔ (φ.Realize v xs ↔ ψ.Reali
 #align first_order.language.bounded_formula.realize_iff FirstOrder.Language.BoundedFormula.realize_iff
 
 theorem realize_castLe_of_eq {m n : ℕ} (h : m = n) {h' : m ≤ n} {φ : L.BoundedFormula α m}
-    {v : α → M} {xs : Fin n → M} : (φ.castLE h').Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h) := by
+    {v : α → M} {xs : Fin n → M} : (φ.castLE h').Realize v xs ↔ φ.Realize v (xs ∘ castIso h) := by
   subst h
-  simp only [castLE_rfl, cast_refl, OrderIso.coe_refl, Function.comp.right_id]
+  simp only [castLE_rfl, castIso_refl, OrderIso.coe_refl, Function.comp.right_id]
 #align first_order.language.bounded_formula.realize_cast_le_of_eq FirstOrder.Language.BoundedFormula.realize_castLe_of_eq
 
 theorem realize_mapTermRel_id [L'.Structure M]
@@ -679,7 +679,7 @@ theorem realize_relabel {φ : L.Formula α} {g : α → β} {v : β → M} :
 theorem realize_relabel_sum_inr (φ : L.Formula (Fin n)) {v : Empty → M} {x : Fin n → M} :
     (BoundedFormula.relabel Sum.inr φ).Realize v x ↔ φ.Realize x := by
   rw [BoundedFormula.realize_relabel, Formula.Realize, Sum.elim_comp_inr, Fin.castAdd_zero,
-    cast_refl, OrderIso.coe_refl, Function.comp.right_id,
+    castIso_refl, OrderIso.coe_refl, Function.comp.right_id,
     Subsingleton.elim (x ∘ (natAdd n : Fin 0 → Fin n)) default]
 #align first_order.language.formula.realize_relabel_sum_inr FirstOrder.Language.Formula.realize_relabel_sum_inr
 
diff --git a/Mathlib/Order/JordanHolder.lean b/Mathlib/Order/JordanHolder.lean
index 4638c4811b99d..fa34456a7fdf1 100644
--- a/Mathlib/Order/JordanHolder.lean
+++ b/Mathlib/Order/JordanHolder.lean
@@ -207,7 +207,7 @@ def toList (s : CompositionSeries X) : List X :=
 /-- Two `CompositionSeries` are equal if they are the same length and
 have the same `i`th element for every `i` -/
 theorem ext_fun {s₁ s₂ : CompositionSeries X} (hl : s₁.length = s₂.length)
-    (h : ∀ i, s₁ i = s₂ (Fin.cast (congr_arg Nat.succ hl) i)) : s₁ = s₂ := by
+    (h : ∀ i, s₁ i = s₂ (Fin.castIso (congr_arg Nat.succ hl) i)) : s₁ = s₂ := by
   cases s₁; cases s₂
   -- Porting note: `dsimp at *` doesn't work. Why?
   dsimp at hl h
@@ -229,7 +229,7 @@ theorem toList_injective : Function.Injective (@CompositionSeries.toList X _ _)
   have h₁ : s₁.length = s₂.length :=
     Nat.succ_injective
       ((List.length_ofFn s₁).symm.trans <| (congr_arg List.length h).trans <| List.length_ofFn s₂)
-  have h₂ : ∀ i : Fin s₁.length.succ, s₁ i = s₂ (Fin.cast (congr_arg Nat.succ h₁) i) :=
+  have h₂ : ∀ i : Fin s₁.length.succ, s₁ i = s₂ (Fin.castIso (congr_arg Nat.succ h₁) i) :=
     -- Porting note: `List.nthLe_ofFn` has been deprecated but `List.get_ofFn` has a
     --               different type, so we do golf here.
     congr_fun <| List.ofFn_injective <| h.trans <| List.ofFn_congr (congr_arg Nat.succ h₁).symm _
@@ -241,7 +241,7 @@ theorem toList_injective : Function.Injective (@CompositionSeries.toList X _ _)
   -- Porting note: `[heq_iff_eq, eq_self_iff_true, true_and_iff]`
   --             → `[mk.injEq, heq_eq_eq, true_and]`
   simp only [mk.injEq, heq_eq_eq, true_and]
-  simp only [Fin.cast_refl] at h₂
+  simp only [Fin.castIso_refl] at h₂
   exact funext h₂
 #align composition_series.to_list_injective CompositionSeries.toList_injective