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

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