F : Type ?u.137488
ι : Type ?u.137491
α : Type u_1
β : Type u_2
γ : Type ?u.137500
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
⊢ Set.Pairwise {x | ∃ a, a ∈ s.val ∧ f a = x} Commute
F : Type ?u.137488
ι : Type ?u.137491
α : Type u_1
β : Type u_2
γ : Type ?u.137500
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
⊢ Set.Pairwise {x | x ∈ Multiset.map f s.val} Commute
simp_rw [Multiset.mem_map]
case intro.intro.intro.intro
F : Type ?u.137488
ι : Type ?u.137491
α : Type u_1
β : Type u_2
γ : Type ?u.137500
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
a : α
ha : a ∈ s.val
b : α
hb : b ∈ s.val
a✝ : f a ≠ f b
⊢ Commute (f a) (f b)
F : Type ?u.137488
ι : Type ?u.137491
α : Type u_1
β : Type u_2
γ : Type ?u.137500
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
⊢ Set.Pairwise {x | ∃ a, a ∈ s.val ∧ f a = x} Commute
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ _
no goals
case intro.intro.intro.intro
F : Type ?u.137488
ι : Type ?u.137491
α : Type u_1
β : Type u_2
γ : Type ?u.137500
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f : α → β
comm : Set.Pairwise ↑s fun a b => Commute (f a) (f b)
a : α
ha : a ∈ s.val
b : α
hb : b ∈ s.val
a✝ : f a ≠ f b
⊢ Commute (f a) (f b)
exact comm.of_refl ha hb