rcases eq_or_lt_of_le (Nat.succ_le_of_lt this) with (h | h)
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
⊢ ↑i + 1 < n
case inl
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
h : Nat.succ ↑i = n
⊢ ↑i + 1 < n

case inr
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
h : Nat.succ ↑i < n
⊢ ↑i + 1 < n