Theorem: Fin.succFin_of_ne (LeanSAT/Upstream/ToMathlib.lean)

State before:
n : ℕ
i : Fin n
⊢ ↑i + 1 ≠ n → ↑i + 1 < n
Tactic:
intro hi
State after:
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
⊢ ↑i + 1 < n

State before:
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
⊢ ↑i + 1 < n
Tactic:
have := i.isLt
State after:
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
⊢ ↑i + 1 < n

State before:
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
⊢ ↑i + 1 < n
Tactic:
rcases eq_or_lt_of_le (Nat.succ_le_of_lt this) with (h | h)
State after:
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

State before:
case inl
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
h : Nat.succ ↑i = n
⊢ ↑i + 1 < n
Tactic:
exact absurd h hi
State after:
no goals

State before:
case inr
n : ℕ
i : Fin n
hi : ↑i + 1 ≠ n
this : ↑i < n
h : Nat.succ ↑i < n
⊢ ↑i + 1 < n
Tactic:
exact h
State after:
no goals