no goals
α : Type u_1
β : Type ?u.10895
γ : Type ?u.10898
M : Type ?u.10901
inst✝¹ : Monoid M
N : Type ?u.10907
inst✝ : Monoid N
xs : List (List α)
⊢ ↑toList (↑ofList (List.join xs)) = ↑toList (List.prod (List.map (↑ofList) xs))
simp