case empty
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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)
comm_ff : Set.Pairwise ↑∅ fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑∅ fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑∅ fun x y => Commute (g x) (f y)
⊢ noncommProd ∅ (f * g) (_ : Set.Pairwise ↑∅ fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd ∅ f comm_ff * noncommProd ∅ g comm_gg

case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
ih :
  ∀ (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)),
    noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
      noncommProd s f comm_ff * noncommProd s g comm_gg
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
⊢ noncommProd (insert x s) (f * g) (_ : Set.Pairwise ↑(insert x s) fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd (insert x s) f comm_ff * noncommProd (insert x s) g comm_gg
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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)
⊢ noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f comm_ff * noncommProd s g comm_gg
induction' s using Finset.induction_on with x s hnmem ih
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
ih :
  ∀ (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)),
    noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
      noncommProd s f comm_ff * noncommProd s g comm_gg
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
⊢ (f * g) x * noncommProd s (f * g) (_ : Set.Pairwise ↑s fun a b => Commute ((f * g) a) ((f * g) b)) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
ih :
  ∀ (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)),
    noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
      noncommProd s f comm_ff * noncommProd s g comm_gg
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
⊢ noncommProd (insert x s) (f * g) (_ : Set.Pairwise ↑(insert x s) fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd (insert x s) f comm_ff * noncommProd (insert x s) g comm_gg
simp only [Finset.noncommProd_insert_of_not_mem _ _ _ _ hnmem]
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ (f * g) x * noncommProd s (f * g) (_ : Set.Pairwise ↑s fun a b => Commute ((f * g) a) ((f * g) b)) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
ih :
  ∀ (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)),
    noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
      noncommProd s f comm_ff * noncommProd s g comm_gg
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
⊢ (f * g) x * noncommProd s (f * g) (_ : Set.Pairwise ↑s fun a b => Commute ((f * g) a) ((f * g) b)) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
specialize
  ih (comm_ff.mono fun _ => mem_insert_of_mem) (comm_gg.mono fun _ => mem_insert_of_mem)
    (comm_gf.mono fun _ => mem_insert_of_mem)
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ f x * g x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ (f * g) x * noncommProd s (f * g) (_ : Set.Pairwise ↑s fun a b => Commute ((f * g) a) ((f * g) b)) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
rw [ih, Pi.mul_apply]
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ f x *
      (g x *
        (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
          noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)))) =
    f x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        (g x * noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))))
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ f x * g x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))) =
    f x * noncommProd s f (_ : Set.Pairwise ↑s fun a b => Commute (f a) (f b)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun a b => Commute (g a) (g b)))
simp only [mul_assoc]
case insert.e_a
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)))
case insert
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ f x *
      (g x *
        (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
          noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)))) =
    f x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        (g x * noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))))
congr 1
case insert.e_a
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x * noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) * g x *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
case insert.e_a
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x *
      (noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
        noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      (g x * noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)))
simp only [← mul_assoc]
case insert.e_a.e_a
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x * noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) * g x
case insert.e_a
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x * noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) * g x *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
congr 1
case insert.e_a.e_a
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)
case insert.e_a.e_a
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
⊢ g x * noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) * g x
refine' noncommProd_commute _ _ _ _ fun y hy => _
no goals
case insert.e_a.e_a
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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 : α
s : Finset α
hnmem : ¬x ∈ s
comm_ff : Set.Pairwise ↑(insert x s) fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑(insert x s) fun x y => Commute (g x) (f y)
ih :
  noncommProd s (f * g) (_ : Set.Pairwise ↑s fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd s f (_ : Set.Pairwise ↑s fun x y => Commute (f x) (f y)) *
      noncommProd s g (_ : Set.Pairwise ↑s fun x y => Commute (g x) (g y))
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)
exact comm_gf (mem_insert_self x s) (mem_insert_of_mem hy) (ne_of_mem_of_not_mem hy hnmem).symm
no goals
case empty
F : Type ?u.219899
ι : Type ?u.219902
α : Type u_1
β : Type u_2
γ : Type ?u.219911
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)
comm_ff : Set.Pairwise ↑∅ fun x y => Commute (f x) (f y)
comm_gg : Set.Pairwise ↑∅ fun x y => Commute (g x) (g y)
comm_gf : Set.Pairwise ↑∅ fun x y => Commute (g x) (f y)
⊢ noncommProd ∅ (f * g) (_ : Set.Pairwise ↑∅ fun x y => Commute ((f * g) x) ((f * g) y)) =
    noncommProd ∅ f comm_ff * noncommProd ∅ g comm_gg
simp