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

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

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

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