case zero
a n : ℕ
⊢ a ^ zero % n = (a % n) ^ zero % n

case succ
a n b : ℕ
ih : a ^ b % n = (a % n) ^ b % n
⊢ a ^ succ b % n = (a % n) ^ succ b % n
a b n : ℕ
⊢ a ^ b % n = (a % n) ^ b % n
induction' b with b ih
case succ
a n b : ℕ
ih : a ^ b % n = (a % n) ^ b % n
⊢ a ^ succ b % n = (a % n) ^ succ b % n
case zero
a n : ℕ
⊢ a ^ zero % n = (a % n) ^ zero % n

case succ
a n b : ℕ
ih : a ^ b % n = (a % n) ^ b % n
⊢ a ^ succ b % n = (a % n) ^ succ b % n
rfl
no goals
case succ
a n b : ℕ
ih : a ^ b % n = (a % n) ^ b % n
⊢ a ^ succ b % n = (a % n) ^ succ b % n
simp [pow_succ, Nat.mul_mod, ih]