n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ (↑Fin.castSucc i) = δ i ≫ δ (Fin.succ i)
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : j = ↑Fin.castSucc i
⊢ δ i ≫ δ j = δ i ≫ δ (Fin.succ i)
subst H
no goals
n : ℕ
i : Fin (n + 2)
⊢ δ i ≫ δ (↑Fin.castSucc i) = δ i ≫ δ (Fin.succ i)
rw [δ_comp_δ_self]