no goals
ι : Type ?u.12132
α : Type ?u.12135
M : Type u_1
N : Type ?u.12141
P : Type ?u.12144
M₀ : Type ?u.12147
G : Type ?u.12150
R : Type ?u.12153
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a✝ a : M
l : List M
⊢ prod (a :: l) = foldr (fun x x_1 => x * x_1) 1 (a :: l)
rw [prod_cons, foldr_cons, prod_eq_foldr]