case inl
n m : ℕ
⊢ ↑(castPred (last (n + 1))) ≤ ↑(last (n + 1))

case inr
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑(castPred i) ≤ ↑i
n m : ℕ
i : Fin (n + 2)
⊢ ↑(castPred i) ≤ ↑i
rcases i.le_last.eq_or_lt with (rfl | h)
no goals
case inl
n m : ℕ
⊢ ↑(castPred (last (n + 1))) ≤ ↑(last (n + 1))
simp
case inr
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑(castLT i (_ : ↑i < n + 1)) ≤ ↑i

case inr.hnc
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ¬↑castSucc (last n) < i
case inr
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑(castPred i) ≤ ↑i
rw [castPred, predAbove, dif_neg]
no goals
case inr
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ↑(castLT i (_ : ↑i < n + 1)) ≤ ↑i
simp
no goals
case inr.hnc
n m : ℕ
i : Fin (n + 2)
h : i < last (n + 1)
⊢ ¬↑castSucc (last n) < i
simpa [lt_iff_val_lt_val, le_iff_val_le_val, lt_succ_iff] using h