F : Type ?u.159067
ι : Type ?u.159070
α : Type ?u.159073
β : Type ?u.159076
γ : Type ?u.159079
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ Set.Pairwise {a} fun a b => Commute (f a) (f b)
F : Type ?u.159067
ι : Type ?u.159070
α : Type ?u.159073
β : Type ?u.159076
γ : Type ?u.159079
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ Set.Pairwise ↑{a} fun a b => Commute (f a) (f b)
norm_cast
no goals
F : Type ?u.159067
ι : Type ?u.159070
α : Type ?u.159073
β : Type ?u.159076
γ : Type ?u.159079
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
a : α
f : α → β
⊢ Set.Pairwise {a} fun a b => Commute (f a) (f b)
exact Set.pairwise_singleton _ _