case h
M : Type u_1
A : Type ?u.28763
B : Type ?u.28766
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
m : Multiset M
comm✝ : Set.Pairwise {x | x ∈ m} Commute
h✝ : ∀ (x : M), x ∈ m → x ∈ S
l : List M
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid M) l} Commute
h : ∀ (x : M), x ∈ Quotient.mk (List.isSetoid M) l → x ∈ S
⊢ Multiset.noncommProd (Quotient.mk (List.isSetoid M) l) comm ∈ S
M : Type u_1
A : Type ?u.28763
B : Type ?u.28766
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
m : Multiset M
comm : Set.Pairwise {x | x ∈ m} Commute
h : ∀ (x : M), x ∈ m → x ∈ S
⊢ Multiset.noncommProd m comm ∈ S
induction' m using Quotient.inductionOn with l
case h
M : Type u_1
A : Type ?u.28763
B : Type ?u.28766
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
m : Multiset M
comm✝ : Set.Pairwise {x | x ∈ m} Commute
h✝ : ∀ (x : M), x ∈ m → x ∈ S
l : List M
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid M) l} Commute
h : ∀ (x : M), x ∈ Quotient.mk (List.isSetoid M) l → x ∈ S
⊢ List.prod l ∈ S
case h
M : Type u_1
A : Type ?u.28763
B : Type ?u.28766
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
m : Multiset M
comm✝ : Set.Pairwise {x | x ∈ m} Commute
h✝ : ∀ (x : M), x ∈ m → x ∈ S
l : List M
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid M) l} Commute
h : ∀ (x : M), x ∈ Quotient.mk (List.isSetoid M) l → x ∈ S
⊢ Multiset.noncommProd (Quotient.mk (List.isSetoid M) l) comm ∈ S
simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]
no goals
case h
M : Type u_1
A : Type ?u.28763
B : Type ?u.28766
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
m : Multiset M
comm✝ : Set.Pairwise {x | x ∈ m} Commute
h✝ : ∀ (x : M), x ∈ m → x ∈ S
l : List M
comm : Set.Pairwise {x | x ∈ Quotient.mk (List.isSetoid M) l} Commute
h : ∀ (x : M), x ∈ Quotient.mk (List.isSetoid M) l → x ∈ S
⊢ List.prod l ∈ S
exact Submonoid.list_prod_mem _ h