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

State before:
m n : ℕ
⊢ (m + 3) ^ n % 3 = m ^ n % 3
Tactic:
induction' n with pn hpn
State after:
case zero
m : ℕ
⊢ (m + 3) ^ 0 % 3 = m ^ 0 % 3

case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) ^ (pn + 1) % 3 = m ^ (pn + 1) % 3

State before:
case zero
m : ℕ
⊢ (m + 3) ^ 0 % 3 = m ^ 0 % 3
Tactic:
simp only [Nat.zero_eq, pow_zero, Nat.one_mod]
State after:
no goals

State before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) ^ (pn + 1) % 3 = m ^ (pn + 1) % 3
Tactic:
rw [Nat.pow_succ']
State after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) * (m + 3) ^ pn % 3 = m ^ (pn + 1) % 3

State before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) * (m + 3) ^ pn % 3 = m ^ (pn + 1) % 3
Tactic:
have h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn := by ring
State after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
⊢ (m + 3) * (m + 3) ^ pn % 3 = m ^ (pn + 1) % 3

State before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
⊢ (m + 3) * (m + 3) ^ pn % 3 = m ^ (pn + 1) % 3
Tactic:
rw [h1]
State after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3

State before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3
Tactic:
have h2 : 3 * (m + 3) ^ pn % 3 = 0 := Nat.mul_mod_right 3 _
State after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3

State before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ (m * (m + 3) ^ pn + 3 * (m + 3) ^ pn) % 3 = m ^ (pn + 1) % 3
Tactic:
rw[Nat.add_mod, h2, add_zero, Nat.mod_mod, Nat.pow_succ']
State after:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ m * (m + 3) ^ pn % 3 = m * m ^ pn % 3

State before:
case succ
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
h1 : (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
h2 : 3 * (m + 3) ^ pn % 3 = 0
⊢ m * (m + 3) ^ pn % 3 = m * m ^ pn % 3
Tactic:
exact Nat.ModEq.mul rfl hpn
State after:
no goals

State before:
m pn : ℕ
hpn : (m + 3) ^ pn % 3 = m ^ pn % 3
⊢ (m + 3) * (m + 3) ^ pn = m * (m + 3) ^ pn + 3 * (m + 3) ^ pn
Tactic:
ring
State after:
no goals