case inl
n m : ℕ
⊢ ↑(castPred (last (n + 1))) < ↑(last (n + 1)) ↔ last (n + 1) = last (n + 1)

case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred i) < ↑i ↔ i = last (n + 1)
n m : ℕ
i : Fin (n + 2)
⊢ ↑(castPred i) < ↑i ↔ i = last (n + 1)
rcases i.le_last.eq_or_lt with (rfl | H)
no goals
case inl
n m : ℕ
⊢ ↑(castPred (last (n + 1))) < ↑(last (n + 1)) ↔ last (n + 1) = last (n + 1)
simp
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred i) < ↑i ↔ False
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred i) < ↑i ↔ i = last (n + 1)
simp only [_root_.ne_of_lt H]
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred (↑castSucc (castPred i))) < ↑(↑castSucc (castPred i)) ↔ False
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred i) < ↑i ↔ False
rw [← castSucc_castPred H]
no goals
case inr
n m : ℕ
i : Fin (n + 2)
H : i < last (n + 1)
⊢ ↑(castPred (↑castSucc (castPred i))) < ↑(↑castSucc (castPred i)) ↔ False
simp