Theorem: LoVe.Even_two_times (LoVe/Labs/Lab5Solution.lean)

State before:
m : ℕ
⊢ Even (2 * (m + 1))
Tactic:
apply Even.add_two
State after:
case a
m : ℕ
⊢ Even (Nat.mul 2 (Nat.add m 0))

State before:
case a
m : ℕ
⊢ Even (Nat.mul 2 (Nat.add m 0))
Tactic:
simp
State after:
case a
m : ℕ
⊢ Even (2 * m)

State before:
case a
m : ℕ
⊢ Even (2 * m)
Tactic:
apply Even_two_times
State after:
no goals