F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute ((f * g) x) ((f * g) y)
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
⊢ Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)
intro x hx y hy h
case hac.hab
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (f y)

case hac.hac
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (g y)

case hbc.hab
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)

case hbc.hac
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute ((f * g) x) ((f * g) y)
apply Commute.mul_left <;> apply Commute.mul_right
no goals
case hac.hab
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (f y)
exact comm_ff.of_refl hx hy
no goals
case hac.hac
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (g y)
exact (comm_gf hy hx h.symm).symm
no goals
case hbc.hab
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)
exact comm_gf hx hy h
no goals
case hbc.hac
F : Type ?u.217198
ι : Type ?u.217201
α : Type u_1
β : Type u_2
γ : Type ?u.217210
f✝ : α → β → β
op : α → α → α
inst✝¹ : Monoid β
inst✝ : Monoid γ
s : Finset α
f g : α → β
comm_ff : Set.Pairwise ↑s fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑s fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑s fun x y => Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)
exact comm_gg.of_refl hx hy