Theorem: Nat.eq_or_lt_of_lt_succ (LeanSAT/Upstream/ToMathlib.lean)

State before:
m n : ℕ
⊢ m < n + 1 → m = n ∨ m < n
Tactic:
intro h
State after:
m n : ℕ
h : m < n + 1
⊢ m = n ∨ m < n

State before:
m n : ℕ
h : m < n + 1
⊢ m = n ∨ m < n
Tactic:
rcases eq_or_lt_of_le (Nat.le_of_lt_succ h) with (rfl | h)
State after:
case inl
m : ℕ
h : m < m + 1
⊢ m = m ∨ m < m

case inr
m n : ℕ
h✝ : m < n + 1
h : m < n
⊢ m = n ∨ m < n

State before:
case inl
m : ℕ
h : m < m + 1
⊢ m = m ∨ m < m
Tactic:
exact Or.inl rfl
State after:
no goals

State before:
case inr
m n : ℕ
h✝ : m < n + 1
h : m < n
⊢ m = n ∨ m < n
Tactic:
exact Or.inr h
State after:
no goals