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