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

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

State before:
⊢ ∃ k, 2 * k = 0
Tactic:
existsi 0
State after:
⊢ 2 * 0 = 0

State before:
⊢ 2 * 0 = 0
Tactic:
numbers
State after:
no goals