F : Type u_1
ι : Type ?u.85305
α : Type u_2
β : Type u_3
γ : Type ?u.85314
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
⊢ Set.Pairwise {x | ∃ a, a ∈ s ∧ ↑f a = x} Commute
F : Type u_1
ι : Type ?u.85305
α : Type u_2
β : Type u_3
γ : Type ?u.85314
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
⊢ Set.Pairwise {x | x ∈ map (↑f) s} Commute
simp only [Multiset.mem_map]
case intro.intro.intro.intro
F : Type u_1
ι : Type ?u.85305
α : Type u_2
β : Type u_3
γ : Type ?u.85314
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a✝ : ↑f x ≠ ↑f y
⊢ Commute (↑f x) (↑f y)
F : Type u_1
ι : Type ?u.85305
α : Type u_2
β : Type u_3
γ : Type ?u.85314
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
⊢ Set.Pairwise {x | ∃ a, a ∈ s ∧ ↑f a = x} Commute
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩ _
no goals
case intro.intro.intro.intro
F : Type u_1
ι : Type ?u.85305
α : Type u_2
β : Type u_3
γ : Type ?u.85314
f✝ : α → β → β
op : α → α → α
inst✝² : Monoid α
inst✝¹ : Monoid β
inst✝ : MonoidHomClass F α β
s : Multiset α
comm : Set.Pairwise {x | x ∈ s} Commute
f : F
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a✝ : ↑f x ≠ ↑f y
⊢ Commute (↑f x) (↑f y)
exact (comm.of_refl hx hy).map f