no goals
ι : Type ?u.67807
α : Type ?u.67810
M : Type u_1
N : Type ?u.67816
P : Type ?u.67819
M₀ : Type ?u.67822
G : Type ?u.67825
R : Type ?u.67828
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l✝ l₁ l₂ : List M
a : M
l : List M
⊢ Option.getD (get? l 0) 1 * prod (tail l) = prod l
cases l <;> simp