no goals
ι : Type ?u.9150
α : Type ?u.9153
M : Type u_1
N : Type ?u.9159
P : Type ?u.9162
M₀ : Type ?u.9165
G : Type ?u.9168
R : Type ?u.9171
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
⊢ prod (concat l a) = prod l * a
rw [concat_eq_append, prod_append, prod_singleton]