Theorem: exists_succ_of_gt (BrownCs22/Homework/Hw8.lean)

State before:
x n : ℕ
⊢ x < n → ∃ n0, n = n0 + 1
Tactic:
intro h
State after:
x n : ℕ
h : x < n
⊢ ∃ n0, n = n0 + 1

State before:
x n : ℕ
h : x < n
⊢ ∃ n0, n = n0 + 1
Tactic:
have hnzp : n = 0 ∨ ∃ n0, n = n0 + 1 := eq_zero_or_exists_succ n
State after:
x n : ℕ
h : x < n
hnzp : n = 0 ∨ ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1

State before:
x n : ℕ
h : x < n
hnzp : n = 0 ∨ ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Tactic:
eliminate hnzp
State after:
case inl
x n : ℕ
h : x < n
h✝ : n = 0
⊢ ∃ n0, n = n0 + 1

case inr
x n : ℕ
h : x < n
h✝ : ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1

State before:
case inl
x n : ℕ
h : x < n
h✝ : n = 0
⊢ ∃ n0, n = n0 + 1

case inr
x n : ℕ
h : x < n
h✝ : ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Tactic:
linarith
State after:
case inr
x n : ℕ
h : x < n
h✝ : ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1

State before:
case inr
x n : ℕ
h : x < n
h✝ : ∃ n0, n = n0 + 1
⊢ ∃ n0, n = n0 + 1
Tactic:
assumption
State after:
no goals