case zero
K : Type u_1
R : Type ?u.348147
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
⊢ a ^ q ^ Nat.zero = a

case succ
K : Type u_1
R : Type ?u.348147
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
n : ℕ
ih : a ^ q ^ n = a
⊢ a ^ q ^ Nat.succ n = a
K : Type u_1
R : Type ?u.348147
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
n : ℕ
a : K
⊢ a ^ q ^ n = a
induction' n with n ih
no goals
case zero
K : Type u_1
R : Type ?u.348147
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
⊢ a ^ q ^ Nat.zero = a
simp
no goals
case succ
K : Type u_1
R : Type ?u.348147
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
n : ℕ
ih : a ^ q ^ n = a
⊢ a ^ q ^ Nat.succ n = a
simp [pow_succ, pow_mul, ih, pow_card]