bump to nightly-2023-07-06-11

mathlib commit leanprover-community/mathlib@5dc6092

Mathbin/Algebra/BigOperators/Fin.lean

@@ -103,16 +103,16 @@ theorem prod_univ_succ [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
 #align fin.sum_univ_succ Fin.sum_univ_succ
 -/
 
-#print Fin.prod_univ_castSucc /-
+#print Fin.prod_univ_castSuccEmb /-
 /-- A product of a function `f : fin (n + 1) → β` over all `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\n`f (fin.last n)` plus the remaining sum"]
-theorem prod_univ_castSucc [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
+theorem prod_univ_castSuccEmb [CommMonoid β] {n : ℕ} (f : Fin (n + 1) → β) :
     ∏ i, f i = (∏ i : Fin n, f i.cast_succ) * f (last n) := by
   simpa [mul_comm] using prod_univ_succ_above 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
 -/
 
 #print Fin.prod_cons /-
@@ -316,9 +316,9 @@ theorem partialProd_right_inv {G : Type _} [Group G] (f : Fin n → G) (i : Fin
   induction' i with i hi generalizing hn
   · simp [-Fin.succ_mk, partial_prod_succ]
   · 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]
-    simp only [partial_prod_succ, mul_inv_rev, Fin.castSucc_mk]
+    simp only [partial_prod_succ, mul_inv_rev, Fin.castSuccEmb_mk]
     assoc_rw [hi, inv_mul_cancel_left]
 #align fin.partial_prod_right_inv Fin.partialProd_right_inv
 #align fin.partial_sum_right_neg Fin.partialSum_right_neg
@@ -371,7 +371,7 @@ def finFunctionFinEquiv {m n : ℕ} : (Fin n → Fin m) ≃ Fin (m ^ n) :=
         · simp
         cases m
         · 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]⟩)
     (fun a b =>
@@ -421,7 +421,7 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
         by
         induction' m with m ih generalizing f
         · 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 <
@@ -430,7 +430,7 @@ def finPiFinEquiv {m : ℕ} {n : Fin m → ℕ} : (∀ i : Fin m, Fin (n i)) ≃
           replace this := 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.init_snoc, Fin.snoc_last, Fin.snoc_init_self n]
+          simp_rw [Fin.snoc_castSuccEmb, Fin.init_snoc, Fin.snoc_last, Fin.snoc_init_self n]
           exact this
         intro n nn f fn
         cases nn

Mathbin/AlgebraicTopology/AlternatingFaceMapComplex.lean

@@ -115,24 +115,24 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 :=
       mul_one, Fin.coe_castLT, Fin.val_succ, pow_one, mul_neg, neg_neg]
     let jj : Fin (n + 2) := (φ (i, j) hij).1
     have ineq : jj ≤ i := by rw [← Fin.val_fin_le]; simpa using hij
-    rw [CategoryTheory.SimplicialObject.δ_comp_δ X ineq, Fin.castSucc_castLT, mul_comm]
+    rw [CategoryTheory.SimplicialObject.δ_comp_δ X ineq, Fin.castSuccEmb_castLT, mul_comm]
   · -- φ : S → Sᶜ is injective
     rintro ⟨i, j⟩ ⟨i', j'⟩ hij hij' h
     rw [Prod.mk.inj_iff]
     refine' ⟨by simpa using congr_arg Prod.snd h, _⟩
-    have h1 := congr_arg Fin.castSucc (congr_arg Prod.fst h)
-    simpa [Fin.castSucc_castLT] using h1
+    have h1 := congr_arg Fin.castSuccEmb (congr_arg Prod.fst h)
+    simpa [Fin.castSuccEmb_castLT] using h1
   · -- φ : S → Sᶜ is surjective
     rintro ⟨i', j'⟩ hij'
     simp only [true_and_iff, Finset.mem_univ, Finset.compl_filter, not_le, Finset.mem_filter] at
       hij' 
-    refine' ⟨(j'.pred _, Fin.castSucc i'), _, _⟩
+    refine' ⟨(j'.pred _, Fin.castSuccEmb i'), _, _⟩
     · intro H
       simpa only [H, Nat.not_lt_zero, Fin.val_zero] using hij'
     ·
-      simpa only [true_and_iff, Finset.mem_univ, Fin.coe_castSucc, Fin.coe_pred,
+      simpa only [true_and_iff, Finset.mem_univ, Fin.coe_castSuccEmb, Fin.coe_pred,
         Finset.mem_filter] using Nat.le_pred_of_lt hij'
-    · simp only [Prod.mk.inj_iff, Fin.succ_pred, Fin.castLT_castSucc]
+    · simp only [Prod.mk.inj_iff, Fin.succ_pred, Fin.castLT_castSuccEmb]
       constructor <;> rfl
 #align algebraic_topology.alternating_face_map_complex.d_squared AlgebraicTopology.AlternatingFaceMapComplex.d_squared
 -/

Mathbin/AlgebraicTopology/DoldKan/Degeneracies.lean

@@ -95,7 +95,7 @@ theorem σ_comp_P_eq_zero (X : SimplicialObject C) {n q : ℕ} (i : Fin (n + 1))
         erw [simplicial_object.δ_comp_σ_self, simplicial_object.δ_comp_σ_self_assoc,
           simplicial_object.δ_comp_σ_succ, comp_id,
           simplicial_object.δ_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]),
           simplicial_object.δ_comp_σ_self_assoc, simplicial_object.δ_comp_σ_succ_assoc]
         abel
       · rw [← id_comp (X.σ i), ← (P_add_Q_f q n.succ : _ = 𝟙 (X.obj _)), add_comp, add_comp]
@@ -112,8 +112,8 @@ 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 ext;
-            simp only [Fin.castSucc_mk, Fin.eta]
+          have hi'' : i = Fin.castSuccEmb ⟨i, by linarith⟩ := by ext;
+            simp only [Fin.castSuccEmb_mk, Fin.eta]
           have eq :=
             hq j.rev.succ
               (by

Mathbin/AlgebraicTopology/DoldKan/Faces.lean

@@ -136,10 +136,10 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
   conv_lhs =>
     congr
     skip
-    rw [Fin.sum_univ_castSucc, Fin.sum_univ_castSucc]
-  rw [Fin.sum_univ_castSucc]
+    rw [Fin.sum_univ_castSuccEmb, Fin.sum_univ_castSuccEmb]
+  rw [Fin.sum_univ_castSuccEmb]
   simp only [Fin.last, Fin.castLE_mk, Fin.coe_castIso, Fin.castIso_mk, Fin.coe_castLE, Fin.val_mk,
-    Fin.castSucc_mk, Fin.coe_castSucc]
+    Fin.castSuccEmb_mk, Fin.coe_castSuccEmb]
   /- the purpose of the following `simplif` is to create three subgoals in order
       to finish the proof -/
   have simplif :
@@ -153,16 +153,17 @@ theorem comp_Hσ_eq {Y : C} {n a q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : HigherFac
     use a
     linarith
   · -- d+e = 0
-    rw [assoc, assoc, X.δ_comp_σ_self' (Fin.castSucc_mk _ _ _).symm,
+    rw [assoc, assoc, 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_smul, add_right_neg]
   · -- c+a = 0
     rw [← Finset.sum_add_distrib]
     apply Finset.sum_eq_zero
     rintro ⟨i, hi⟩ h₀
-    have hia : (⟨i, by linarith⟩ : Fin (n + 2)) ≤ Fin.castSucc (⟨a, by linarith⟩ : Fin (n + 1)) :=
-      by simpa only [Fin.le_iff_val_le_val, Fin.val_mk, Fin.castSucc_mk, ← lt_succ_iff] using hi
-    simp only [Fin.val_mk, Fin.castLE_mk, Fin.castSucc_mk, Fin.succ_mk, assoc, Fin.castIso_mk, ←
+    have hia :
+      (⟨i, by linarith⟩ : Fin (n + 2)) ≤ Fin.castSuccEmb (⟨a, by linarith⟩ : Fin (n + 1)) := by
+      simpa only [Fin.le_iff_val_le_val, Fin.val_mk, Fin.castSuccEmb_mk, ← lt_succ_iff] using hi
+    simp only [Fin.val_mk, Fin.castLE_mk, Fin.castSuccEmb_mk, Fin.succ_mk, assoc, Fin.castIso_mk, ←
       δ_comp_σ_of_le X hia, add_eq_zero_iff_eq_neg, ← neg_zsmul]
     congr
     ring
@@ -181,8 +182,8 @@ theorem comp_Hσ_eq_zero {Y : C} {n q : ℕ} {φ : Y ⟶ X _[n + 1]} (v : Higher
       Fin.mk_zero, one_zsmul, eq_to_hom_refl, comp_id, comp_sum,
       alternating_face_map_complex.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]

Mathbin/AlgebraicTopology/SimplexCategory.lean

@@ -327,7 +327,7 @@ theorem δ_comp_σ_of_le {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : i ≤ j.ca
   rcases i with ⟨i, _⟩
   rcases j with ⟨j, _⟩
   rcases k with ⟨k, _⟩
-  simp only [Fin.mk_le_mk, Fin.castSucc_mk] at H 
+  simp only [Fin.mk_le_mk, Fin.castSuccEmb_mk] at H 
   dsimp
   split_ifs
   -- Most of the goals can now be handled by `linarith`,
@@ -353,8 +353,8 @@ theorem δ_comp_σ_self {n} {i : Fin (n + 1)} : δ i.cast_succ ≫ σ i = 𝟙 [
   by
   ext j
   suffices
-    ite (Fin.castSucc i < ite (j < i) (Fin.castSucc j) j.succ) (ite (j < i) (j : ℕ) (j + 1) - 1)
-        (ite (j < i) j (j + 1)) =
+    ite (Fin.castSuccEmb i < ite (j < i) (Fin.castSuccEmb j) j.succ)
+        (ite (j < i) (j : ℕ) (j + 1) - 1) (ite (j < i) j (j + 1)) =
       j
     by dsimp [δ, σ, Fin.succAbove, Fin.predAbove]; simpa [Fin.predAbove, push_cast]
   rcases i with ⟨i, _⟩
@@ -402,10 +402,10 @@ theorem δ_comp_σ_of_gt {n} {i : Fin (n + 2)} {j : Fin (n + 1)} (H : j.cast_suc
   rcases i with ⟨i, _⟩
   rcases j with ⟨j, _⟩
   rcases k with ⟨k, _⟩
-  simp only [Fin.mk_lt_mk, Fin.castSucc_mk] at H 
+  simp only [Fin.mk_lt_mk, Fin.castSuccEmb_mk] at H 
   suffices
     ite (_ < ite (k < i + 1) _ _) _ _ = ite _ (ite (j < k) (k - 1) k) (ite (j < k) (k - 1) k + 1) by
-    simpa [apply_dite Fin.castSucc, Fin.predAbove, push_cast]
+    simpa [apply_dite Fin.castSuccEmb, Fin.predAbove, push_cast]
   split_ifs
   -- Most of the goals can now be handled by `linarith`,
   -- but we have to deal with three of them by hand.
@@ -447,7 +447,7 @@ theorem δ_comp_σ_of_gt' {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ <
   by
   rw [← δ_comp_σ_of_gt]
   · simpa only [Fin.succ_pred]
-  · rw [Fin.castSucc_castLT, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
+  · rw [Fin.castSuccEmb_castLT, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
     exact H
 #align simplex_category.δ_comp_σ_of_gt' SimplexCategory.δ_comp_σ_of_gt'
 -/
@@ -697,13 +697,13 @@ instance {n : ℕ} {i : Fin (n + 1)} : Epi (σ i) :=
   simp only [σ, mk_hom, hom.to_order_hom_mk, OrderHom.coe_fun_mk]
   by_cases b ≤ i
   · use b
-    rw [Fin.predAbove_below i b (by simpa only [Fin.coe_eq_castSucc] using h)]
-    simp only [Fin.coe_eq_castSucc, Fin.castPred_castSucc]
+    rw [Fin.predAbove_below i b (by simpa only [Fin.coe_eq_castSuccEmb] using h)]
+    simp only [Fin.coe_eq_castSuccEmb, Fin.castPred_castSuccEmb]
   · use b.succ
     rw [Fin.predAbove_above i b.succ _, Fin.pred_succ]
     rw [not_le] at h 
     rw [Fin.lt_iff_val_lt_val] at h ⊢
-    simpa only [Fin.val_succ, Fin.coe_castSucc] using Nat.lt.step h
+    simpa only [Fin.val_succ, Fin.coe_castSuccEmb] using Nat.lt.step h
 
 instance : ReflectsIsomorphisms (forget SimplexCategory) :=
   ⟨by
@@ -780,9 +780,9 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk
     small_category_comp, σ, mk_hom, OrderHom.coe_fun_mk]
   by_cases h' : x ≤ i.cast_succ
   · rw [Fin.predAbove_below i x h']
-    have eq := Fin.castSucc_castPred (gt_of_gt_of_ge (Fin.castSucc_lt_last i) h')
+    have eq := Fin.castSuccEmb_castPred (gt_of_gt_of_ge (Fin.castSuccEmb_lt_last i) h')
     erw [Fin.succAbove_below i.succ x.cast_pred _]; swap
-    · rwa [Eq, ← Fin.le_castSucc_iff]
+    · rwa [Eq, ← Fin.le_castSuccEmb_iff]
     rw [Eq]
   · simp only [not_le] at h' 
     let y :=
@@ -799,7 +799,7 @@ theorem eq_σ_comp_of_not_injective' {n : ℕ} {Δ' : SimplexCategory} (θ : mk
       erw [Fin.succAbove_below i.succ _]
       exact Fin.lt_succ
     · erw [Fin.succAbove_above i.succ _]
-      simp only [Fin.lt_iff_val_lt_val, Fin.le_iff_val_le_val, Fin.val_succ, Fin.coe_castSucc,
+      simp only [Fin.lt_iff_val_lt_val, Fin.le_iff_val_le_val, Fin.val_succ, Fin.coe_castSuccEmb,
         Nat.lt_succ_iff, Fin.ext_iff] at h' h'' ⊢
       cases' Nat.le.dest h' with c hc
       cases c
@@ -833,11 +833,11 @@ theorem eq_σ_comp_of_not_injective {n : ℕ} {Δ' : SimplexCategory} (θ : mk (
   let z := x.cast_pred
   use z
   simp only [←
-    show z.cast_succ = x from Fin.castSucc_castPred (lt_of_lt_of_le h₂ (Fin.le_last y))] at h₁ h₂ 
+    show z.cast_succ = x from Fin.castSuccEmb_castPred (lt_of_lt_of_le h₂ (Fin.le_last y))] at h₁ h₂ 
   apply eq_σ_comp_of_not_injective'
-  rw [Fin.castSucc_lt_iff_succ_le] at h₂ 
+  rw [Fin.castSuccEmb_lt_iff_succ_le] at h₂ 
   apply le_antisymm
-  · exact θ.to_order_hom.monotone (le_of_lt (Fin.castSucc_lt_succ z))
+  · exact θ.to_order_hom.monotone (le_of_lt (Fin.castSuccEmb_lt_succ z))
   · rw [h₁]
     exact θ.to_order_hom.monotone h₂
 #align simplex_category.eq_σ_comp_of_not_injective SimplexCategory.eq_σ_comp_of_not_injective
@@ -855,28 +855,28 @@ theorem eq_comp_δ_of_not_surjective' {n : ℕ} {Δ : SimplexCategory} (θ : Δ
     by_cases h' : θ.to_order_hom x ≤ i
     · simp only [σ, mk_hom, hom.to_order_hom_mk, OrderHom.coe_fun_mk]
       rw [Fin.predAbove_below (Fin.castPred i) (θ.to_order_hom x)
-          (by simpa [Fin.castSucc_castPred h] using h')]
+          (by simpa [Fin.castSuccEmb_castPred h] using h')]
       erw [Fin.succAbove_below i]; swap
-      · simp only [Fin.lt_iff_val_lt_val, Fin.coe_castSucc]
+      · simp only [Fin.lt_iff_val_lt_val, Fin.coe_castSuccEmb]
         exact
           lt_of_le_of_lt (Fin.coe_castPred_le_self _)
             (fin.lt_iff_coe_lt_coe.mp ((Ne.le_iff_lt (hi x)).mp h'))
-      rw [Fin.castSucc_castPred]
+      rw [Fin.castSuccEmb_castPred]
       apply lt_of_le_of_lt h' h
     · simp only [not_le] at h' 
       simp only [σ, mk_hom, hom.to_order_hom_mk, OrderHom.coe_fun_mk,
         Fin.predAbove_above (Fin.castPred i) (θ.to_order_hom x)
-          (by simpa only [Fin.castSucc_castPred h] using h')]
+          (by simpa only [Fin.castSuccEmb_castPred h] using h')]
       erw [Fin.succAbove_above i _, Fin.succ_pred]
-      simpa only [Fin.le_iff_val_le_val, Fin.coe_castSucc, Fin.coe_pred] using
+      simpa only [Fin.le_iff_val_le_val, Fin.coe_castSuccEmb, Fin.coe_pred] using
         Nat.le_pred_of_lt (fin.lt_iff_coe_lt_coe.mp h')
   · obtain rfl := le_antisymm (Fin.le_last i) (not_lt.mp h)
     use θ ≫ σ (Fin.last _)
     ext1; ext1; ext1 x
     simp only [hom.to_order_hom_mk, Function.comp_apply, OrderHom.comp_coe, hom.comp,
       small_category_comp, σ, δ, mk_hom, OrderHom.coe_fun_mk, OrderEmbedding.toOrderHom_coe,
       Fin.predAbove_last, Fin.succAbove_last,
-      Fin.castSucc_castPred ((Ne.le_iff_lt (hi x)).mp (Fin.le_last _))]
+      Fin.castSuccEmb_castPred ((Ne.le_iff_lt (hi x)).mp (Fin.le_last _))]
 #align simplex_category.eq_comp_δ_of_not_surjective' SimplexCategory.eq_comp_δ_of_not_surjective'
 -/
 

Mathbin/Analysis/SchwartzSpace.lean

@@ -1091,7 +1091,7 @@ theorem iteratedPDeriv_succ_right {n : ℕ} (m : Fin (n + 1) → E) (f : 𝓢(E,
   · rw [iterated_pderiv_zero, iterated_pderiv_one]
     rfl
   -- The proof is `∂^{n + 2} = ∂ ∂^{n + 1} = ∂ ∂^n ∂ = ∂^{n+1} ∂`
-  have hmzero : Fin.init m 0 = m 0 := by simp only [Fin.init_def, Fin.castSucc_zero]
+  have hmzero : Fin.init m 0 = m 0 := by simp only [Fin.init_def, Fin.castSuccEmb_zero]
   have hmtail : Fin.tail m (Fin.last n) = m (Fin.last n.succ) := by
     simp only [Fin.tail_def, Fin.succ_last]
   simp only [iterated_pderiv_succ_left, IH (Fin.tail m), hmzero, hmtail, Fin.tail_init_eq_init_tail]

Mathbin/Data/Array/Lemmas.lean

@@ -284,15 +284,15 @@ theorem read_pushBack_left (i : Fin n) : (a.pushBack v).read i.cast_succ = a.rea
   by
   cases' i with i hi
   have : ¬i = n := ne_of_lt hi
-  simp [push_back, this, Fin.castSucc, Fin.castAdd, Fin.castLE, Fin.castLT, read, DArray.read]
+  simp [push_back, this, Fin.castSuccEmb, Fin.castAdd, Fin.castLE, Fin.castLT, read, DArray.read]
 #align array.read_push_back_left Array'.read_pushBack_left
 
 @[simp]
 theorem read_pushBack_right : (a.pushBack v).read (Fin.last _) = v :=
   by
   cases' hn : Fin.last n with k hk
   have : k = n := by simpa [Fin.eq_iff_veq] using hn.symm
-  simp [push_back, this, Fin.castSucc, Fin.castAdd, Fin.castLE, Fin.castLT, read, DArray.read]
+  simp [push_back, this, Fin.castSuccEmb, Fin.castAdd, Fin.castLE, Fin.castLT, read, DArray.read]
 #align array.read_push_back_right Array'.read_pushBack_right
 
 end PushBack