case zero
ι : Type ?u.13701
α : Type ?u.13704
M : Type u_1
N : Type ?u.13710
P : Type ?u.13713
M₀ : Type ?u.13716
G : Type ?u.13719
R : Type ?u.13722
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
⊢ prod (replicate Nat.zero a) = a ^ Nat.zero

case succ
ι : Type ?u.13701
α : Type ?u.13704
M : Type u_1
N : Type ?u.13710
P : Type ?u.13713
M₀ : Type ?u.13716
G : Type ?u.13719
R : Type ?u.13722
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
n : ℕ
ih : prod (replicate n a) = a ^ n
⊢ prod (replicate (Nat.succ n) a) = a ^ Nat.succ n
ι : Type ?u.13701
α : Type ?u.13704
M : Type u_1
N : Type ?u.13710
P : Type ?u.13713
M₀ : Type ?u.13716
G : Type ?u.13719
R : Type ?u.13722
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ : M
n : ℕ
a : M
⊢ prod (replicate n a) = a ^ n
induction' n with n ih
case zero
ι : Type ?u.13701
α : Type ?u.13704
M : Type u_1
N : Type ?u.13710
P : Type ?u.13713
M₀ : Type ?u.13716
G : Type ?u.13719
R : Type ?u.13722
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
⊢ prod (replicate Nat.zero a) = 1
case zero
ι : Type ?u.13701
α : Type ?u.13704
M : Type u_1
N : Type ?u.13710
P : Type ?u.13713
M₀ : Type ?u.13716
G : Type ?u.13719
R : Type ?u.13722
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
⊢ prod (replicate Nat.zero a) = a ^ Nat.zero
rw [pow_zero]
no goals
case zero
ι : Type ?u.13701
α : Type ?u.13704
M : Type u_1
N : Type ?u.13710
P : Type ?u.13713
M₀ : Type ?u.13716
G : Type ?u.13719
R : Type ?u.13722
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
⊢ prod (replicate Nat.zero a) = 1
rfl
no goals
case succ
ι : Type ?u.13701
α : Type ?u.13704
M : Type u_1
N : Type ?u.13710
P : Type ?u.13713
M₀ : Type ?u.13716
G : Type ?u.13719
R : Type ?u.13722
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a✝ a : M
n : ℕ
ih : prod (replicate n a) = a ^ n
⊢ prod (replicate (Nat.succ n) a) = a ^ Nat.succ n
rw [replicate_succ, prod_cons, ih, pow_succ]