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

State before:
⊢ ∀ (n : ℕ), MyOdd (n + 1) → MyEven n
Tactic:
intro n
State after:
n : ℕ
⊢ MyOdd (n + 1) → MyEven n

State before:
n : ℕ
⊢ MyOdd (n + 1) → MyEven n
Tactic:
dsimp [MyEven, MyOdd]
State after:
n : ℕ
⊢ (∃ k, 2 * k + 1 = n + 1) → ∃ k, 2 * k = n

State before:
n : ℕ
⊢ (∃ k, 2 * k + 1 = n + 1) → ∃ k, 2 * k = n
Tactic:
intro h
State after:
n : ℕ
h : ∃ k, 2 * k + 1 = n + 1
⊢ ∃ k, 2 * k = n

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

State before:
case intro
n x : ℕ
hx : 2 * x + 1 = n + 1
⊢ ∃ k, 2 * k = n
Tactic:
existsi x
State after:
case intro
n x : ℕ
hx : 2 * x + 1 = n + 1
⊢ 2 * x = n

State before:
case intro
n x : ℕ
hx : 2 * x + 1 = n + 1
⊢ 2 * x = n
Tactic:
linarith
State after:
no goals