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

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

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

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

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

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