case h
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
⊢ ∀ (x : M), x ∈ Multiset.map f t.val → x ∈ S
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
⊢ Finset.noncommProd t f comm ∈ S
apply multiset_noncommProd_mem
case h
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
y : M
⊢ y ∈ Multiset.map f t.val → y ∈ S
case h
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
⊢ ∀ (x : M), x ∈ Multiset.map f t.val → x ∈ S
intro y
case h
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
y : M
⊢ (∃ a, a ∈ t.val ∧ f a = y) → y ∈ S
case h
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
y : M
⊢ y ∈ Multiset.map f t.val → y ∈ S
rw [Multiset.mem_map]
case h.intro.intro
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S
case h
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
y : M
⊢ (∃ a, a ∈ t.val ∧ f a = y) → y ∈ S
rintro ⟨x, ⟨hx, rfl⟩⟩
no goals
case h.intro.intro
M : Type u_1
A : Type ?u.31592
B : Type ?u.31595
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S✝ : B
s S : Submonoid M
ι : Type u_2
t : Finset ι
f : ι → M
comm : Set.Pairwise ↑t fun a b => Commute (f a) (f b)
h : ∀ (c : ι), c ∈ t → f c ∈ S
x : ι
hx : x ∈ t.val
⊢ f x ∈ S
exact h x hx