-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
R : Type u_3
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : NonUnitalSemiring R
x y z : R⟦Γ⟧
b : Γ
coeff :
  ∀ (a : (_ : Γ × Γ) × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      Membership.mem (α := (_ : Γ × Γ) × Γ × Γ) (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support) (t := y.support + z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) ⋯ ⋯ a.2)
        (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j) :
          (_ : Γ × Γ) × Γ × Γ)
coeff₁ :
  ∀ (a : (_ : Γ × Γ) × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support) (t := y.support + z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) ⋯ ⋯ a.2)
        a →
      Membership.mem (α := (_ : Γ × Γ) × Γ × Γ) (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (i + k, l) (i, k) :
          (_ : Γ × Γ) × Γ × Γ)
coeff₂ :
  ∀ (a : (_ : Γ × Γ) × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ)
          match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j) with
        | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (i + k, l) (i, k)) =
        a
coeff₃ :
  ∀ (a : (_ : Γ × Γ) × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support) (t := y.support + z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) ⋯ ⋯ a.2)
        a →
      (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ)
          match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (i + k, l) (i, k) with
        | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j)) =
        a
coeff₄ :
  ∀ (a : (_ : Γ × Γ) × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ) × Γ × Γ))
        ((addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      x.coeff a.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * y.coeff a.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2 *
          z.coeff a.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).2 =
        x.coeff
            (Sigma.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ)
                (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
                | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j))).1 *
          (y.coeff
              (Sigma.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ)
                  (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
                  | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j))).1 *
            z.coeff
              (Sigma.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ)
                  (match (motive := (_ : Γ × Γ) × Γ × Γ → (_ : Γ × Γ) × Γ × Γ) a with
                  | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ) ↦ Γ × Γ) (k, l + j) (l, j))).2)
⊢ Eq.{u_3 + 1} (α := R)
    (∑
      x_1 ∈
        (addAntidiagonal (s := x.support + y.support) (t := z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1,
      x.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * y.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2 *
        z.coeff x_1.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).2)
    (∑
      x_1 ∈
        (addAntidiagonal (s := x.support) (t := y.support + z.support) ⋯ ⋯ b).sigma (α := fun (a : Γ × Γ) ↦ Γ × Γ)
          fun (a : Γ × Γ) ↦ addAntidiagonal (s := y.support) (t := z.support) ⋯ ⋯ a.2,
      x.coeff x_1.fst (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 *
        (y.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).1 * z.coeff x_1.snd (β := fun (i : Γ × Γ) ↦ Γ × Γ).2))

Tactic:
apply Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩)
    (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩)

Premises used: Finset.sum_nbij'