case h
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y : β
h : ∀ (x : α), x ∈ s → Commute y (f x)
⊢ ∀ (x : β), x ∈ Multiset.map f s.val → Commute y x
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y : β
h : ∀ (x : α), x ∈ s → Commute y (f x)
⊢ Commute y (noncommProd s f comm)
apply Multiset.noncommProd_commute
case h
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y✝ : β
h : ∀ (x : α), x ∈ s → Commute y✝ (f x)
y : β
⊢ y ∈ Multiset.map f s.val → Commute y✝ y
case h
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y : β
h : ∀ (x : α), x ∈ s → Commute y (f x)
⊢ ∀ (x : β), x ∈ Multiset.map f s.val → Commute y x
intro y
case h
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y✝ : β
h : ∀ (x : α), x ∈ s → Commute y✝ (f x)
y : β
⊢ (∃ a, a ∈ s.val ∧ f a = y) → Commute y✝ y
case h
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y✝ : β
h : ∀ (x : α), x ∈ s → Commute y✝ (f x)
y : β
⊢ y ∈ Multiset.map f s.val → Commute y✝ y
rw [Multiset.mem_map]
case h.intro.intro
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y : β
h : ∀ (x : α), x ∈ s → Commute y (f x)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)
case h
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y✝ : β
h : ∀ (x : α), x ∈ s → Commute y✝ (f x)
y : β
⊢ (∃ a, a ∈ s.val ∧ f a = y) → Commute y✝ y
rintro ⟨x, ⟨hx, rfl⟩⟩
no goals
case h.intro.intro
F : Type ?u.196819
ι : Type ?u.196822
α : Type u_1
β : Type u_2
γ : Type ?u.196831
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
y : β
h : ∀ (x : α), x ∈ s → Commute y (f x)
x : α
hx : x ∈ s.val
⊢ Commute y (f x)
exact h x hx