Theorem: Bulgaria1998P11.foo1 (Compfiles/Bulgaria1998P11.lean)

State before:
m n : ℕ
ho : Odd m
⊢ (m + 3) ^ n.succ % 2 = 0
Tactic:
cases' ho with w hw
State after:
case intro
m n w : ℕ
hw : m = 2 * w + 1
⊢ (m + 3) ^ n.succ % 2 = 0

State before:
case intro
m n w : ℕ
hw : m = 2 * w + 1
⊢ (m + 3) ^ n.succ % 2 = 0
Tactic:
rw[hw, Nat.pow_succ, show 2 * w + 1 + 3 = 2 * (w + 2) by ring, Nat.mul_mod,
   Nat.mul_mod_right, mul_zero, Nat.zero_mod]
State after:
no goals

State before:
m n w : ℕ
hw : m = 2 * w + 1
⊢ 2 * w + 1 + 3 = 2 * (w + 2)
Tactic:
ring
State after:
no goals