no goals
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
hj : j = 0
⊢ False
simp [hj, Fin.not_lt_zero] at H
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
⊢ δ i ≫ δ j = δ i ≫ δ (Fin.succ (Fin.pred j (_ : j = 0 → False)))

n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
⊢ i ≤ Fin.pred j (_ : j = 0 → False)
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
⊢ δ i ≫ δ j = δ (Fin.pred j (_ : j = 0 → False)) ≫ δ (↑Fin.castSucc i)
rw [← δ_comp_δ]
no goals
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
⊢ δ i ≫ δ j = δ i ≫ δ (Fin.succ (Fin.pred j (_ : j = 0 → False)))
rw [Fin.succ_pred]
no goals
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : ↑Fin.castSucc i < j
⊢ i ≤ Fin.pred j (_ : j = 0 → False)
simpa only [Fin.le_iff_val_le_val, ← Nat.lt_succ_iff, Nat.succ_eq_add_one, ← Fin.val_succ,
  j.succ_pred, Fin.lt_iff_val_lt_val] using H