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

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

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

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

State before:
case intro
x : ℕ
h : 2 * x = 1
⊢ False
Tactic:
rewrite [@Nat.mul_eq_one_iff] at h
State after:
case intro
x : ℕ
h : 2 = 1 ∧ x = 1
⊢ False

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