no goals
ι : Type ?u.1915
α : Type ?u.1918
M : Type u_1
N : Type ?u.1924
P : Type ?u.1927
M₀ : Type ?u.1930
G : Type ?u.1933
R : Type ?u.1936
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
⊢ prod (a :: l) = foldl (fun x x_1 => x * x_1) (a * 1) l
simp only [List.prod, foldl_cons, one_mul, mul_one]