F : Type ?u.139635
ι : Type ?u.139638
α : Type ?u.139641
β : Type ?u.139644
γ : Type ?u.139647
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (g x) (g y)
F : Type ?u.139635
ι : Type ?u.139638
α : Type ?u.139641
β : Type ?u.139644
γ : Type ?u.139647
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ (fun a b => Commute (g a) (g b)) x y
dsimp only
F : Type ?u.139635
ι : Type ?u.139638
α : Type ?u.139641
β : Type ?u.139644
γ : Type ?u.139647
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)
F : Type ?u.139635
ι : Type ?u.139638
α : Type ?u.139641
β : Type ?u.139644
γ : Type ?u.139647
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (g x) (g y)
rw [← h₂ _ hx, ← h₂ _ hy]
F : Type ?u.139635
ι : Type ?u.139638
α : Type ?u.139641
β : Type ?u.139644
γ : Type ?u.139647
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ : Finset α
f g : α → β
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x y : α
h : x ≠ y
h₂ : ∀ (x : α), x ∈ s₁ → f x = g x
hx : x ∈ ↑s₁
hy : y ∈ ↑s₁
⊢ Commute (f x) (f y)
F : Type ?u.139635
ι : Type ?u.139638
α : Type ?u.139641
β : Type ?u.139644
γ : Type ?u.139647
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x : α
hx : x ∈ ↑s₂
y : α
hy : y ∈ ↑s₂
h : x ≠ y
⊢ Commute (f x) (f y)
subst h₁
no goals
F : Type ?u.139635
ι : Type ?u.139638
α : Type ?u.139641
β : Type ?u.139644
γ : Type ?u.139647
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ : Finset α
f g : α → β
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
x y : α
h : x ≠ y
h₂ : ∀ (x : α), x ∈ s₁ → f x = g x
hx : x ∈ ↑s₁
hy : y ∈ ↑s₁
⊢ Commute (f x) (f y)
exact comm hx hy h
no goals
F : Type ?u.139635
ι : Type ?u.139638
α : Type u_1
β : Type u_2
γ : Type ?u.139647
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ (x : α), x ∈ s₂ → f x = g x
comm : Set.Pairwise ↑s₁ fun a b => Commute (f a) (f b)
⊢ noncommProd s₁ f comm =
    noncommProd s₂ g (_ : ∀ (x : α), x ∈ ↑s₂ → ∀ (y : α), y ∈ ↑s₂ → x ≠ y → (fun a b => Commute (g a) (g b)) x y)
simp_rw [noncommProd, Multiset.map_congr (congr_arg _ h₁) h₂]