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

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

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

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

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

State before:
case intro
n x : ℕ
hx : 2 * x = n + 1
⊢ ∃ k, 2 * k + 1 = n
Tactic:
cases x with
| zero => {apply False.elim; simp at hx; linarith}
| succ x => {existsi x; linarith}
State after:
no goals

State before:
case intro.zero
n : ℕ
hx : 2 * Nat.zero = n + 1
⊢ ∃ k, 2 * k + 1 = n
Tactic:
apply False.elim
State after:
case intro.zero.h
n : ℕ
hx : 2 * Nat.zero = n + 1
⊢ False

State before:
case intro.zero.h
n : ℕ
hx : 2 * Nat.zero = n + 1
⊢ False
Tactic:
simp at hx
State after:
case intro.zero.h
n : ℕ
hx : 0 = n + 1
⊢ False

State before:
case intro.zero.h
n : ℕ
hx : 0 = n + 1
⊢ False
Tactic:
linarith
State after:
no goals

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

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