case intro
M : Type u_1
A : Type ?u.11708
B : Type u_2
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List { x // x ∈ S }
⊢ List.prod (List.map Subtype.val l) ∈ S
M : Type u_1
A : Type ?u.11708
B : Type u_2
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
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.11708
B : Type u_2
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List { x // x ∈ S }
⊢ ↑(List.prod l) ∈ S
case intro
M : Type u_1
A : Type ?u.11708
B : Type u_2
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
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.11708
B : Type u_2
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List { x // x ∈ S }
⊢ ↑(List.prod l) ∈ S
exact l.prod.coe_prop