Theorem: Hw7.zero_isnt_odd (BrownCs22/Homework/Hw7.lean)

State before:
⊢ ¬MyOdd 0
Tactic:
dsimp [MyOdd]
State after:
⊢ ¬∃ k, 2 * k + 1 = 0

State before:
⊢ ¬∃ k, 2 * k + 1 = 0
Tactic:
intro h
State after:
h : ∃ k, 2 * k + 1 = 0
⊢ False

State before:
h : ∃ k, 2 * k + 1 = 0
⊢ False
Tactic:
eliminate h with x h
State after:
case intro
x : ℕ
h : 2 * x + 1 = 0
⊢ False

State before:
case intro
x : ℕ
h : 2 * x + 1 = 0
⊢ False
Tactic:
linarith
State after:
no goals