no goals
ι : Type ?u.10461
α : Type ?u.10464
M : Type u_1
N : Type ?u.10470
P : Type ?u.10473
M₀ : Type ?u.10476
G : Type ?u.10479
R : Type ?u.10482
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List (List M)
⊢ prod (join l) = prod (map prod l)
induction l <;> [rfl; simp only [*, List.join, map, prod_append, prod_cons]]