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

State before:
n : ℕ
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
have hnzp : n = 0 ∨ n > 0 := Nat.eq_zero_or_pos n
State after:
n : ℕ
hnzp : n = 0 ∨ n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1

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

case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1

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

case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
{left; assumption}
State after:
case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1

State before:
case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
{
  right
  eliminate (Nat.exists_eq_succ_of_ne_zero (by linarith)) with w
  existsi w
  assumption
}
State after:
no goals

State before:
case inl
n : ℕ
h✝ : n = 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
left
State after:
case inl.h
n : ℕ
h✝ : n = 0
⊢ n = 0

State before:
case inl.h
n : ℕ
h✝ : n = 0
⊢ n = 0
Tactic:
assumption
State after:
no goals

State before:
case inr
n : ℕ
h✝ : n > 0
⊢ n = 0 ∨ ∃ n0, n = n0 + 1
Tactic:
right
State after:
case inr.h
n : ℕ
h✝ : n > 0
⊢ ∃ n0, n = n0 + 1

State before:
case inr.h
n : ℕ
h✝ : n > 0
⊢ ∃ n0, n = n0 + 1
Tactic:
eliminate (Nat.exists_eq_succ_of_ne_zero (by linarith)) with w
State after:
case inr.h.intro
n : ℕ
h✝¹ : n > 0
w : ℕ
h✝ : n = Nat.succ w
⊢ ∃ n0, n = n0 + 1

State before:
case inr.h.intro
n : ℕ
h✝¹ : n > 0
w : ℕ
h✝ : n = Nat.succ w
⊢ ∃ n0, n = n0 + 1
Tactic:
existsi w
State after:
case inr.h.intro
n : ℕ
h✝¹ : n > 0
w : ℕ
h✝ : n = Nat.succ w
⊢ n = w + 1

State before:
case inr.h.intro
n : ℕ
h✝¹ : n > 0
w : ℕ
h✝ : n = Nat.succ w
⊢ n = w + 1
Tactic:
assumption
State after:
no goals

State before:
n : ℕ
h✝ : n > 0
⊢ ?m.18553 ≠ 0
Tactic:
linarith
State after:
no goals