no goals
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type ?u.47396
inst✝ : AddMonoid A
t : Set A
hs : IsSubmonoid s
a : M
l : List M
h : ∀ (x : M), x ∈ a :: l → x ∈ s
this : a * List.prod l ∈ s
⊢ List.prod (a :: l) ∈ s
simpa
no goals
M : Type u_1
inst✝¹ : Monoid M
s : Set M
A : Type ?u.47396
inst✝ : AddMonoid A
t : Set A
hs : IsSubmonoid s
a : M
l : List M
h : ∀ (x : M), x ∈ a :: l → x ∈ s
⊢ a ∈ s ∧ ∀ (x : M), x ∈ l → x ∈ s
simpa using h