case intro
M : Type u_1
A : Type ?u.25243
B : Type ?u.25246
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
s : Submonoid M
l : List { x // x ∈ s }
⊢ List.prod (List.map Subtype.val l) ∈ s
M : Type u_1
A : Type ?u.25243
B : Type ?u.25246
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
s : Submonoid M
l : List M
hl : ∀ (x : M), x ∈ l → x ∈ s
⊢ List.prod l ∈ s
lift l to List s using hl
case intro
M : Type u_1
A : Type ?u.25243
B : Type ?u.25246
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
s : Submonoid M
l : List { x // x ∈ s }
⊢ ↑(List.prod l) ∈ s
case intro
M : Type u_1
A : Type ?u.25243
B : Type ?u.25246
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
s : Submonoid M
l : List { x // x ∈ s }
⊢ List.prod (List.map Subtype.val l) ∈ s
rw [← coe_list_prod]
no goals
case intro
M : Type u_1
A : Type ?u.25243
B : Type ?u.25246
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
s : Submonoid M
l : List { x // x ∈ s }
⊢ ↑(List.prod l) ∈ s
exact l.prod.coe_prop