-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_mul_distrib {s : Finset α} (f : α → β) (g : α → β) (comm_ff comm_gg comm_gf) :
    noncommProd s (f * g) (noncommProd_mul_distrib_aux comm_ff comm_gg comm_gf) =
      noncommProd s f comm_ff * noncommProd s g comm_gg

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnmem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnmem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnmem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnmem)).Pairwise fun x y => Commute (g x) (f y)
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)

Tactic:
exact comm_gf (mem_cons_self x s) (mem_cons_of_mem hy) (ne_of_mem_of_not_mem hy hnmem).symm

Result:
no goals

Proof state:
case h₁
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
comm_ff : (↑∅).Pairwise (Commute on f)
comm_gg : (↑∅).Pairwise (Commute on g)
comm_gf : (↑∅).Pairwise fun x y => Commute (g x) (f y)
⊢ ∅.noncommProd (f * g) ⋯ = ∅.noncommProd f comm_ff * ∅.noncommProd g comm_gg

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)
⊢ s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg

Tactic:
induction' s using Finset.cons_induction_on with x s hnmem ih

Result:
case h₁
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
comm_ff : (↑∅).Pairwise (Commute on f)
comm_gg : (↑∅).Pairwise (Commute on g)
comm_gf : (↑∅).Pairwise fun x y => Commute (g x) (f y)
⊢ ∅.noncommProd (f * g) ⋯ = ∅.noncommProd f comm_ff * ∅.noncommProd g comm_gg

case h₂
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnmem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnmem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnmem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnmem)).Pairwise fun x y => Commute (g x) (f y)
⊢ (cons x s hnmem).noncommProd (f * g) ⋯ =
    (cons x s hnmem).noncommProd f comm_ff * (cons x s hnmem).noncommProd g comm_gg

Proof state:
case h₂
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnmem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnmem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnmem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnmem)).Pairwise fun x y => Commute (g x) (f y)
⊢ (cons x s hnmem).noncommProd (f * g) ⋯ =
    (cons x s hnmem).noncommProd f comm_ff * (cons x s hnmem).noncommProd g comm_gg

Tactic:
rw [Finset.noncommProd_cons, Finset.noncommProd_cons, Finset.noncommProd_cons, Pi.mul_apply,
  ih (comm_ff.mono fun _ => mem_cons_of_mem) (comm_gg.mono fun _ => mem_cons_of_mem)
    (comm_gf.mono fun _ => mem_cons_of_mem),
  (noncommProd_commute _ _ _ _ fun y hy => ?_).mul_mul_mul_comm]

Result:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
x : α
s : Finset α
hnmem : x ∉ s
ih :
  ∀ (comm_ff : (↑s).Pairwise (Commute on f)) (comm_gg : (↑s).Pairwise (Commute on g))
    (comm_gf : (↑s).Pairwise fun x y => Commute (g x) (f y)),
    s.noncommProd (f * g) ⋯ = s.noncommProd f comm_ff * s.noncommProd g comm_gg
comm_ff : (↑(cons x s hnmem)).Pairwise (Commute on f)
comm_gg : (↑(cons x s hnmem)).Pairwise (Commute on g)
comm_gf : (↑(cons x s hnmem)).Pairwise fun x y => Commute (g x) (f y)
y : α
hy : y ∈ s
⊢ Commute (g x) (f y)