no goals
ι : Type ?u.5270
α : Type ?u.5273
M : Type u_1
N : Type ?u.5279
P : Type ?u.5282
M₀ : Type ?u.5285
G : Type ?u.5288
R : Type ?u.5291
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
⊢ prod (l₁ ++ l₂) = foldl (fun x x_1 => x * x_1) (foldl (fun x x_1 => x * x_1) 1 l₁ * 1) l₂
simp [List.prod]