diff --git a/src/Init/Data/BitVec/Basic.lean b/src/Init/Data/BitVec/Basic.lean
index f509f7b03a..44c883f746 100644
--- a/src/Init/Data/BitVec/Basic.lean
+++ b/src/Init/Data/BitVec/Basic.lean
@@ -351,17 +351,17 @@ end relations
 section cast
 
 /-- `cast eq x` embeds `x` into an equal `BitVec` type. -/
-@[inline] def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLt x.toNat (eq ▸ x.isLt)
+@[inline] protected def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLt x.toNat (eq ▸ x.isLt)
 
 @[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
-    cast h (BitVec.ofNat n x) = BitVec.ofNat m x := by
+    (BitVec.ofNat n x).cast h = BitVec.ofNat m x := by
   subst h; rfl
 
 @[simp] theorem cast_cast {n m k : Nat} (h₁ : n = m) (h₂ : m = k) (x : BitVec n) :
-    cast h₂ (cast h₁ x) = cast (h₁ ▸ h₂) x :=
+    (x.cast h₁).cast h₂ = x.cast (h₁ ▸ h₂) :=
   rfl
 
-@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) : cast h x = x := rfl
+@[simp] theorem cast_eq {n : Nat} (h : n = n) (x : BitVec n) : x.cast h = x := rfl
 
 /--
 Extraction of bits `start` to `start + len - 1` from a bit vector of size `n` to yield a
diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 21523d5f87..590bfcb7a7 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -410,21 +410,21 @@ theorem toNat_ge_of_msb_true {x : BitVec n} (p : BitVec.msb x = true) : x.toNat
 
 /-! ### cast -/
 
-@[simp, bv_toNat] theorem toNat_cast (h : w = v) (x : BitVec w) : (cast h x).toNat = x.toNat := rfl
+@[simp, bv_toNat] theorem toNat_cast (h : w = v) (x : BitVec w) : (x.cast h).toNat = x.toNat := rfl
 @[simp] theorem toFin_cast (h : w = v) (x : BitVec w) :
-    (cast h x).toFin = x.toFin.cast (by rw [h]) :=
+    (x.cast h).toFin = x.toFin.cast (by rw [h]) :=
   rfl
 
-@[simp] theorem getLsbD_cast (h : w = v) (x : BitVec w) : (cast h x).getLsbD i = x.getLsbD i := by
+@[simp] theorem getLsbD_cast (h : w = v) (x : BitVec w) : (x.cast h).getLsbD i = x.getLsbD i := by
   subst h; simp
 
-@[simp] theorem getMsbD_cast (h : w = v) (x : BitVec w) : (cast h x).getMsbD i = x.getMsbD i := by
+@[simp] theorem getMsbD_cast (h : w = v) (x : BitVec w) : (x.cast h).getMsbD i = x.getMsbD i := by
   subst h; simp
 
-@[simp] theorem getElem_cast (h : w = v) (x : BitVec w) (p : i < v) : (cast h x)[i] = x[i] := by
+@[simp] theorem getElem_cast (h : w = v) (x : BitVec w) (p : i < v) : (x.cast h)[i] = x[i] := by
   subst h; simp
 
-@[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (cast h x).msb = x.msb := by
+@[simp] theorem msb_cast (h : w = v) (x : BitVec w) : (x.cast h).msb = x.msb := by
   simp [BitVec.msb]
 
 /-! ### toInt/ofInt -/
@@ -658,7 +658,7 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
     <;> omega
 
 @[simp] theorem cast_setWidth (h : v = v') (x : BitVec w) :
-    cast h (setWidth v x) = setWidth v' x := by
+    (x.setWidth v).cast h = x.setWidth v' := by
   subst h
   ext
   simp
@@ -671,7 +671,7 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
   revert p
   cases getLsbD x i <;> simp; omega
 
-@[simp] theorem setWidth_cast {h : w = v} : (cast h x).setWidth k = x.setWidth k := by
+@[simp] theorem setWidth_cast {x : BitVec w} {h : w = v} : (x.cast h).setWidth k = x.setWidth k := by
   apply eq_of_getLsbD_eq
   simp
 
@@ -1102,19 +1102,19 @@ theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
 
 /-! ### cast -/
 
-@[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by
+@[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(x.cast h) = (~~~x).cast h := by
   ext
   simp_all [lt_of_getLsbD]
 
-@[simp] theorem and_cast {x y : BitVec w} (h : w = w') : cast h x &&& cast h y = cast h (x &&& y) := by
+@[simp] theorem and_cast {x y : BitVec w} (h : w = w') : x.cast h &&& y.cast h = (x &&& y).cast h := by
   ext
   simp_all [lt_of_getLsbD]
 
-@[simp] theorem or_cast {x y : BitVec w} (h : w = w') : cast h x ||| cast h y = cast h (x ||| y) := by
+@[simp] theorem or_cast {x y : BitVec w} (h : w = w') : x.cast h ||| y.cast h = (x ||| y).cast h := by
   ext
   simp_all [lt_of_getLsbD]
 
-@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : cast h x ^^^ cast h y = cast h (x ^^^ y) := by
+@[simp] theorem xor_cast {x y : BitVec w} (h : w = w') : x.cast h ^^^ y.cast h = (x ^^^ y).cast h := by
   ext
   simp_all [lt_of_getLsbD]
 
@@ -1797,7 +1797,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   rw [getLsbD_append] -- Why does this not work with `simp [getLsbD_append]`?
   simp
 
-@[simp] theorem zero_width_append (x : BitVec 0) (y : BitVec v) : x ++ y = cast (by omega) y := by
+@[simp] theorem zero_width_append (x : BitVec 0) (y : BitVec v) : x ++ y = y.cast (by omega) := by
   ext
   rw [getLsbD_append]
   simpa using lt_of_getLsbD
@@ -1807,7 +1807,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
 
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
-    cast h (x ++ y) = x ++ cast (by omega) y := by
+    (x ++ y).cast h = x ++ y.cast (by omega) := by
   ext
   simp only [getLsbD_cast, getLsbD_append, cond_eq_if, decide_eq_true_eq]
   split <;> split
@@ -1818,7 +1818,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
     omega
 
 @[simp] theorem cast_append_left (h : w + v = w' + v) (x : BitVec w) (y : BitVec v) :
-    cast h (x ++ y) = cast (by omega) x ++ y := by
+    (x ++ y).cast h = x.cast (by omega) ++ y := by
   ext
   simp [getLsbD_append]
 
diff --git a/src/Init/Data/Fin/Basic.lean b/src/Init/Data/Fin/Basic.lean
index 33df16cc40..48a5d12c7a 100644
--- a/src/Init/Data/Fin/Basic.lean
+++ b/src/Init/Data/Fin/Basic.lean
@@ -176,7 +176,7 @@ protected theorem pos (i : Fin n) : 0 < n :=
 @[inline] def castLE (h : n ≤ m) (i : Fin n) : Fin m := ⟨i, Nat.lt_of_lt_of_le i.2 h⟩
 
 /-- `cast eq i` embeds `i` into an equal `Fin` type. -/
-@[inline] def cast (eq : n = m) (i : Fin n) : Fin m := ⟨i, eq ▸ i.2⟩
+@[inline] protected def cast (eq : n = m) (i : Fin n) : Fin m := ⟨i, eq ▸ i.2⟩
 
 /-- `castAdd m i` embeds `i : Fin n` in `Fin (n+m)`. See also `Fin.natAdd` and `Fin.addNat`. -/
 @[inline] def castAdd (m) : Fin n → Fin (n + m) :=
diff --git a/src/Init/Data/Fin/Lemmas.lean b/src/Init/Data/Fin/Lemmas.lean
index 03521a8900..803515dee3 100644
--- a/src/Init/Data/Fin/Lemmas.lean
+++ b/src/Init/Data/Fin/Lemmas.lean
@@ -370,25 +370,25 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
     Fin.castLE mn ∘ Fin.castLE km = Fin.castLE (Nat.le_trans km mn) :=
   funext (castLE_castLE km mn)
 
-@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (cast h i : Nat) = i := rfl
+@[simp] theorem coe_cast (h : n = m) (i : Fin n) : (i.cast h : Nat) = i := rfl
 
-@[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : cast h (last n) = last n' :=
+@[simp] theorem cast_last {n' : Nat} {h : n + 1 = n' + 1} : (last n).cast h  = last n' :=
   Fin.ext (by rw [coe_cast, val_last, val_last, Nat.succ.inj h])
 
-@[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
+@[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : Fin.cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
 
-@[simp] theorem cast_refl (n : Nat) (h : n = n) : cast h = id := by
+@[simp] theorem cast_refl (n : Nat) (h : n = n) : Fin.cast h = id := by
   ext
   simp
 
 @[simp] theorem cast_trans {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
-    cast h' (cast h i) = cast (Eq.trans h h') i := rfl
+    (i.cast h).cast h' = i.cast (Eq.trans h h') := rfl
 
 theorem castLE_of_eq {m n : Nat} (h : m = n) {h' : m ≤ n} : castLE h' = Fin.cast h := rfl
 
 @[simp] theorem coe_castAdd (m : Nat) (i : Fin n) : (castAdd m i : Nat) = i := rfl
 
-@[simp] theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = cast rfl := rfl
+@[simp] theorem castAdd_zero : (castAdd 0 : Fin n → Fin (n + 0)) = Fin.cast rfl := rfl
 
 theorem castAdd_lt {m : Nat} (n : Nat) (i : Fin m) : (castAdd n i : Nat) < m := by simp
 
@@ -406,37 +406,37 @@ theorem castAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
     castAdd m (Fin.cast h i) = Fin.cast (congrArg (. + m) h) (castAdd m i) := Fin.ext rfl
 
 theorem cast_castAdd_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
-    cast h (castAdd m i) = castAdd m (cast (Nat.add_right_cancel h) i) := rfl
+    (i.castAdd m).cast h = (i.cast (Nat.add_right_cancel h)).castAdd m := rfl
 
 @[simp] theorem cast_castAdd_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
-    cast h (castAdd m' i) = castAdd m i := rfl
+    (i.castAdd m').cast h = i.castAdd m := rfl
 
 theorem castAdd_castAdd {m n p : Nat} (i : Fin m) :
-    castAdd p (castAdd n i) = cast (Nat.add_assoc ..).symm (castAdd (n + p) i) := rfl
+    (i.castAdd n).castAdd p = (i.castAdd (n + p)).cast (Nat.add_assoc ..).symm  := rfl
 
 /-- The cast of the successor is the successor of the cast. See `Fin.succ_cast_eq` for rewriting in
 the reverse direction. -/
 @[simp] theorem cast_succ_eq {n' : Nat} (i : Fin n) (h : n.succ = n'.succ) :
-    cast h i.succ = (cast (Nat.succ.inj h) i).succ := rfl
+    i.succ.cast h = (i.cast (Nat.succ.inj h)).succ := rfl
 
 theorem succ_cast_eq {n' : Nat} (i : Fin n) (h : n = n') :
-    (cast h i).succ = cast (by rw [h]) i.succ := rfl
+    (i.cast h).succ = i.succ.cast (by rw [h]) := rfl
 
-@[simp] theorem coe_castSucc (i : Fin n) : (Fin.castSucc i : Nat) = i := rfl
+@[simp] theorem coe_castSucc (i : Fin n) : (i.castSucc : Nat) = i := rfl
 
 @[simp] theorem castSucc_mk (n i : Nat) (h : i < n) : castSucc ⟨i, h⟩ = ⟨i, Nat.lt.step h⟩ := rfl
 
 @[simp] theorem cast_castSucc {n' : Nat} {h : n + 1 = n' + 1} {i : Fin n} :
-    cast h (castSucc i) = castSucc (cast (Nat.succ.inj h) i) := rfl
+    i.castSucc.cast h = (i.cast (Nat.succ.inj h)).castSucc := rfl
 
-theorem castSucc_lt_succ (i : Fin n) : Fin.castSucc i < i.succ :=
+theorem castSucc_lt_succ (i : Fin n) : i.castSucc < i.succ :=
   lt_def.2 <| by simp only [coe_castSucc, val_succ, Nat.lt_succ_self]
 
-theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ Fin.castSucc j ↔ i < j.succ := by
+theorem le_castSucc_iff {i : Fin (n + 1)} {j : Fin n} : i ≤ j.castSucc ↔ i < j.succ := by
   simpa only [lt_def, le_def] using Nat.add_one_le_add_one_iff.symm
 
 theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
-    Fin.castSucc i < j ↔ i.succ ≤ j := .rfl
+    i.castSucc < j ↔ i.succ ≤ j := .rfl
 
 @[simp] theorem succ_last (n : Nat) : (last n).succ = last n.succ := rfl
 
@@ -444,48 +444,48 @@ theorem castSucc_lt_iff_succ_le {n : Nat} {i : Fin n} {j : Fin (n + 1)} :
     i.succ = last (n + 1) ↔ i = last n := by rw [← succ_last, succ_inj]
 
 @[simp] theorem castSucc_castLT (i : Fin (n + 1)) (h : (i : Nat) < n) :
-    castSucc (castLT i h) = i := rfl
+    (castLT i h).castSucc = i := rfl
 
 @[simp] theorem castLT_castSucc {n : Nat} (a : Fin n) (h : (a : Nat) < n) :
-    castLT (castSucc a) h = a := rfl
+    castLT a.castSucc h = a := rfl
 
 @[simp] theorem castSucc_lt_castSucc_iff {a b : Fin n} :
-    Fin.castSucc a < Fin.castSucc b ↔ a < b := .rfl
+    a.castSucc < b.castSucc ↔ a < b := .rfl
 
-theorem castSucc_inj {a b : Fin n} : castSucc a = castSucc b ↔ a = b := by simp [Fin.ext_iff]
+theorem castSucc_inj {a b : Fin n} : a.castSucc = b.castSucc ↔ a = b := by simp [Fin.ext_iff]
 
-theorem castSucc_lt_last (a : Fin n) : castSucc a < last n := a.is_lt
+theorem castSucc_lt_last (a : Fin n) : a.castSucc < last n := a.is_lt
 
 @[simp] theorem castSucc_zero : castSucc (0 : Fin (n + 1)) = 0 := rfl
 
 @[simp] theorem castSucc_one {n : Nat} : castSucc (1 : Fin (n + 2)) = 1 := rfl
 
 /-- `castSucc i` is positive when `i` is positive -/
-theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < castSucc i := by
+theorem castSucc_pos {i : Fin (n + 1)} (h : 0 < i) : 0 < i.castSucc := by
   simpa [lt_def] using h
 
-@[simp] theorem castSucc_eq_zero_iff {a : Fin (n + 1)} : castSucc a = 0 ↔ a = 0 := by simp [Fin.ext_iff]
+@[simp] theorem castSucc_eq_zero_iff {a : Fin (n + 1)} : a.castSucc = 0 ↔ a = 0 := by simp [Fin.ext_iff]
 
-theorem castSucc_ne_zero_iff {a : Fin (n + 1)} : castSucc a ≠ 0 ↔ a ≠ 0 :=
+theorem castSucc_ne_zero_iff {a : Fin (n + 1)} : a.castSucc ≠ 0 ↔ a ≠ 0 :=
   not_congr <| castSucc_eq_zero_iff
 
 theorem castSucc_fin_succ (n : Nat) (j : Fin n) :
-    castSucc (Fin.succ j) = Fin.succ (castSucc j) := by simp [Fin.ext_iff]
+    j.succ.castSucc = (j.castSucc).succ := by simp [Fin.ext_iff]
 
 @[simp]
-theorem coeSucc_eq_succ {a : Fin n} : castSucc a + 1 = a.succ := by
+theorem coeSucc_eq_succ {a : Fin n} : a.castSucc + 1 = a.succ := by
   cases n
   · exact a.elim0
   · simp [Fin.ext_iff, add_def, Nat.mod_eq_of_lt (Nat.succ_lt_succ a.is_lt)]
 
-theorem lt_succ {a : Fin n} : castSucc a < a.succ := by
+theorem lt_succ {a : Fin n} : a.castSucc < a.succ := by
   rw [castSucc, lt_def, coe_castAdd, val_succ]; exact Nat.lt_succ_self a.val
 
 theorem exists_castSucc_eq {n : Nat} {i : Fin (n + 1)} : (∃ j, castSucc j = i) ↔ i ≠ last n :=
   ⟨fun ⟨j, hj⟩ => hj ▸ Fin.ne_of_lt j.castSucc_lt_last,
    fun hi => ⟨i.castLT <| Fin.val_lt_last hi, rfl⟩⟩
 
-theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = castSucc i.succ := rfl
+theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = i.succ.castSucc := rfl
 
 @[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
 
@@ -502,17 +502,17 @@ theorem le_coe_addNat (m : Nat) (i : Fin n) : m ≤ addNat i m :=
     addNat ⟨i, hi⟩ n = ⟨i + n, Nat.add_lt_add_right hi n⟩ := rfl
 
 @[simp] theorem cast_addNat_zero {n n' : Nat} (i : Fin n) (h : n + 0 = n') :
-    cast h (addNat i 0) = cast ((Nat.add_zero _).symm.trans h) i := rfl
+    (addNat i 0).cast h = i.cast ((Nat.add_zero _).symm.trans h) := rfl
 
 /-- For rewriting in the reverse direction, see `Fin.cast_addNat_left`. -/
 theorem addNat_cast {n n' m : Nat} (i : Fin n') (h : n' = n) :
-    addNat (cast h i) m = cast (congrArg (. + m) h) (addNat i m) := rfl
+    addNat (i.cast h) m = (addNat i m).cast (congrArg (. + m) h) := rfl
 
 theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
-    cast h (addNat i m) = addNat (cast (Nat.add_right_cancel h) i) m := rfl
+    (addNat i m).cast h = addNat (i.cast (Nat.add_right_cancel h)) m := rfl
 
 @[simp] theorem cast_addNat_right {n m m' : Nat} (i : Fin n) (h : n + m' = n + m) :
-    cast h (addNat i m') = addNat i m :=
+    (addNat i m').cast h = addNat i m :=
   Fin.ext <| (congrArg ((· + ·) (i : Nat)) (Nat.add_left_cancel h) : _)
 
 @[simp] theorem coe_natAdd (n : Nat) {m : Nat} (i : Fin m) : (natAdd n i : Nat) = n + i := rfl
@@ -522,46 +522,46 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
 
 theorem le_coe_natAdd (m : Nat) (i : Fin n) : m ≤ natAdd m i := Nat.le_add_right ..
 
-@[simp] theorem natAdd_zero {n : Nat} : natAdd 0 = cast (Nat.zero_add n).symm := by ext; simp
+@[simp] theorem natAdd_zero {n : Nat} : natAdd 0 = Fin.cast (Nat.zero_add n).symm := by ext; simp
 
 /-- For rewriting in the reverse direction, see `Fin.cast_natAdd_right`. -/
 theorem natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
-    natAdd m (cast h i) = cast (congrArg _ h) (natAdd m i) := rfl
+    natAdd m (i.cast h) = (natAdd m i).cast (congrArg _ h) := rfl
 
 theorem cast_natAdd_right {n n' m : Nat} (i : Fin n') (h : m + n' = m + n) :
-    cast h (natAdd m i) = natAdd m (cast (Nat.add_left_cancel h) i) := rfl
+    (natAdd m i).cast h  = natAdd m (i.cast (Nat.add_left_cancel h)) := rfl
 
 @[simp] theorem cast_natAdd_left {n m m' : Nat} (i : Fin n) (h : m' + n = m + n) :
-    cast h (natAdd m' i) = natAdd m i :=
+    (natAdd m' i).cast h = natAdd m i :=
   Fin.ext <| (congrArg (· + (i : Nat)) (Nat.add_right_cancel h) : _)
 
 theorem castAdd_natAdd (p m : Nat) {n : Nat} (i : Fin n) :
-    castAdd p (natAdd m i) = cast (Nat.add_assoc ..).symm (natAdd m (castAdd p i)) := rfl
+    castAdd p (natAdd m i) = (natAdd m (castAdd p i)).cast (Nat.add_assoc ..).symm := rfl
 
 theorem natAdd_castAdd (p m : Nat) {n : Nat} (i : Fin n) :
-    natAdd m (castAdd p i) = cast (Nat.add_assoc ..) (castAdd p (natAdd m i)) := rfl
+    natAdd m (castAdd p i) = (castAdd p (natAdd m i)).cast (Nat.add_assoc ..) := rfl
 
 theorem natAdd_natAdd (m n : Nat) {p : Nat} (i : Fin p) :
-    natAdd m (natAdd n i) = cast (Nat.add_assoc ..) (natAdd (m + n) i) :=
+    natAdd m (natAdd n i) = (natAdd (m + n) i).cast (Nat.add_assoc ..) :=
   Fin.ext <| (Nat.add_assoc ..).symm
 
 @[simp]
 theorem cast_natAdd_zero {n n' : Nat} (i : Fin n) (h : 0 + n = n') :
-    cast h (natAdd 0 i) = cast ((Nat.zero_add _).symm.trans h) i :=
+    (natAdd 0 i).cast h = i.cast ((Nat.zero_add _).symm.trans h) :=
   Fin.ext <| Nat.zero_add _
 
 @[simp]
 theorem cast_natAdd (n : Nat) {m : Nat} (i : Fin m) :
-    cast (Nat.add_comm ..) (natAdd n i) = addNat i n := Fin.ext <| Nat.add_comm ..
+    (natAdd n i).cast (Nat.add_comm ..) = addNat i n := Fin.ext <| Nat.add_comm ..
 
 @[simp]
 theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
-    cast (Nat.add_comm ..) (addNat i m) = natAdd m i := Fin.ext <| Nat.add_comm ..
+    (addNat i m).cast (Nat.add_comm ..) = natAdd m i := Fin.ext <| Nat.add_comm ..
 
 @[simp] theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := rfl
 
 @[simp] theorem addNat_last (n : Nat) :
-    addNat (last n) m = cast (by omega) (last (n + m)) := by
+    addNat (last n) m = (last (n + m)).cast (by omega) := by
   ext
   simp
 
@@ -657,7 +657,7 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
     subNat m (addNat i m) h = i := Fin.ext <| Nat.add_sub_cancel i m
 
 @[simp] theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
-    natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [← cast_addNat]
+    natAdd n (subNat n (i.cast (Nat.add_comm ..)) h) = i := by simp [← cast_addNat]
 
 /-! ### recursion and induction principles -/