n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ ↑Fin.castSucc j
⊢ δ j ≫ δ (↑Fin.castSucc (Fin.castLT i (_ : ↑i < n + 2))) = δ j ≫ δ i

n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ ↑Fin.castSucc j
⊢ Fin.castLT i (_ : ↑i < n + 2) ≤ j
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ ↑Fin.castSucc j
⊢ δ (Fin.castLT i (_ : ↑i < n + 2)) ≫ δ (Fin.succ j) = δ j ≫ δ i
rw [δ_comp_δ]
no goals
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ ↑Fin.castSucc j
⊢ δ j ≫ δ (↑Fin.castSucc (Fin.castLT i (_ : ↑i < n + 2))) = δ j ≫ δ i
rfl
no goals
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ ↑Fin.castSucc j
⊢ Fin.castLT i (_ : ↑i < n + 2) ≤ j
exact H