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

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

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

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

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

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