no goals
ι : Type ?u.48568
α : Type ?u.48571
M : Type u_1
N : Type ?u.48577
P : Type ?u.48580
M₀ : Type ?u.48583
G : Type ?u.48586
R : Type ?u.48589
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a : M
x✝ : ∀ (m : M), m ∈ [] → IsUnit m
⊢ IsUnit (prod [])
simp
ι : Type ?u.48568
α : Type ?u.48571
M : Type u_1
N : Type ?u.48577
P : Type ?u.48580
M₀ : Type ?u.48583
G : Type ?u.48586
R : Type ?u.48589
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (h * prod t)
ι : Type ?u.48568
α : Type ?u.48571
M : Type u_1
N : Type ?u.48577
P : Type ?u.48580
M₀ : Type ?u.48583
G : Type ?u.48586
R : Type ?u.48589
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (prod (h :: t))
simp only [List.prod_cons]
no goals
ι : Type ?u.48568
α : Type ?u.48571
M : Type u_1
N : Type ?u.48577
P : Type ?u.48580
M₀ : Type ?u.48583
G : Type ?u.48586
R : Type ?u.48589
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
l l₁ l₂ : List M
a h : M
t : List M
u : ∀ (m : M), m ∈ h :: t → IsUnit m
⊢ IsUnit (h * prod t)
exact IsUnit.mul (u h (mem_cons_self h t)) (prod_isUnit fun m mt => u m (mem_cons_of_mem h mt))