Theorem: even_mul_add_one (LeanTeaching/TD/TD02.lean)

State before:
n : ℕ
⊢ Even (n * (n + 1))
Tactic:
cases (even_or_odd n) with
| inl heven =>
 
  exact Even.mul_right heven (n + 1)
| inr hodd =>
  have hsucc : Even (n + 1) := by
   rw [even_add_one, ← odd_iff_not_even]
   exact hodd
  exact Even.mul_left hsucc n
State after:
no goals

State before:
case inl
n : ℕ
heven : Even n
⊢ Even (n * (n + 1))
Tactic:
exact Even.mul_right heven (n + 1)
State after:
no goals

State before:
case inr
n : ℕ
hodd : Odd n
⊢ Even (n * (n + 1))
Tactic:
have hsucc : Even (n + 1) := by
 rw [even_add_one, ← odd_iff_not_even]
 exact hodd
State after:
case inr
n : ℕ
hodd : Odd n
hsucc : Even (n + 1)
⊢ Even (n * (n + 1))

State before:
case inr
n : ℕ
hodd : Odd n
hsucc : Even (n + 1)
⊢ Even (n * (n + 1))
Tactic:
exact Even.mul_left hsucc n
State after:
no goals

State before:
n : ℕ
hodd : Odd n
⊢ Even (n + 1)
Tactic:
rw [even_add_one, ← odd_iff_not_even]
State after:
n : ℕ
hodd : Odd n
⊢ Odd n

State before:
n : ℕ
hodd : Odd n
⊢ Odd n
Tactic:
exact hodd
State after:
no goals