F : Type ?u.179852
α : Type u_1
β : Type ?u.179858
γ : Type ?u.179861
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
⊢ ↑(npowRec n s) = ↑s ^ n
F : Type ?u.179852
α : Type u_1
β : Type ?u.179858
γ : Type ?u.179861
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
⊢ ↑(s ^ n) = ↑s ^ n
change ↑(npowRec n s) = (s: Set α) ^ n
case zero
F : Type ?u.179852
α : Type u_1
β : Type ?u.179858
γ : Type ?u.179861
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n : ℕ
s : Finset α
⊢ ↑(npowRec Nat.zero s) = ↑s ^ Nat.zero

case succ
F : Type ?u.179852
α : Type u_1
β : Type ?u.179858
γ : Type ?u.179861
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (Nat.succ n) s) = ↑s ^ Nat.succ n
F : Type ?u.179852
α : Type u_1
β : Type ?u.179858
γ : Type ?u.179861
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
⊢ ↑(npowRec n s) = ↑s ^ n
induction' n with n ih
no goals
case zero
F : Type ?u.179852
α : Type u_1
β : Type ?u.179858
γ : Type ?u.179861
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n : ℕ
s : Finset α
⊢ ↑(npowRec Nat.zero s) = ↑s ^ Nat.zero
rw [npowRec, pow_zero, coe_one]
no goals
case succ
F : Type ?u.179852
α : Type u_1
β : Type ?u.179858
γ : Type ?u.179861
inst✝² : DecidableEq α
inst✝¹ : DecidableEq β
inst✝ : Monoid α
s✝ t : Finset α
a : α
m n✝ : ℕ
s : Finset α
n : ℕ
ih : ↑(npowRec n s) = ↑s ^ n
⊢ ↑(npowRec (Nat.succ n) s) = ↑s ^ Nat.succ n
rw [npowRec, pow_succ, coe_mul, ih]