-- Module: Mathlib.RingTheory.HahnSeries.Multiplication
Goal:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_5
inst : AddCommMonoid Γ
inst_1 : PartialOrder Γ
inst_2 : IsOrderedCancelAddMonoid Γ
inst_3 : PartialOrder Γ'
inst_4 : AddAction Γ Γ'
inst_5 : IsOrderedCancelVAdd Γ Γ'
inst_6 : AddCommMonoid V
inst_7 : Semiring R
inst_8 : Module R V
x y : R⟦Γ⟧
z : HahnModule Γ' R V
b : Γ'
h :
  ∀ (a : (_ : Γ × Γ') × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ))
        ((VAddAntidiagonal (s := x.support + y.support) (t :=
              HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) b
              ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      Membership.mem (α := (_ : Γ × Γ') × Γ × Γ') (γ := Finset ((_ : Γ × Γ') × Γ × Γ'))
        ((VAddAntidiagonal (s := x.support) (t :=
              HVAdd.hVAdd (β := Set Γ') y.support
                (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
              b ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ') fun (a : Γ × Γ') ↦
          VAddAntidiagonal (s := y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a.2 ⋯)
        (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j) :
          (_ : Γ × Γ') × Γ × Γ')
h₁ :
  ∀ (a : (_ : Γ × Γ') × Γ × Γ'),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ'))
        ((VAddAntidiagonal (s := x.support) (t :=
              HVAdd.hVAdd (β := Set Γ') y.support
                (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
              b ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ') fun (a : Γ × Γ') ↦
          VAddAntidiagonal (s := y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a.2 ⋯)
        a →
      Membership.mem (α := (_ : Γ × Γ') × Γ × Γ) (γ := Finset ((_ : Γ × Γ') × Γ × Γ))
        ((VAddAntidiagonal (s := x.support + y.support) (t :=
              HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) 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) :
          (_ : Γ × Γ') × Γ × Γ)
h₂ :
  ∀ (a : (_ : Γ × Γ') × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ))
        ((VAddAntidiagonal (s := x.support + y.support) (t :=
              HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) 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
h₃ :
  ∀ (a : (_ : Γ × Γ') × Γ × Γ'),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ'))
        ((VAddAntidiagonal (s := x.support) (t :=
              HVAdd.hVAdd (β := Set Γ') y.support
                (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
              b ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ') fun (a : Γ × Γ') ↦
          VAddAntidiagonal (s := y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) 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
h₄ :
  ∀ (a : (_ : Γ × Γ') × Γ × Γ),
    Membership.mem (γ := Finset ((_ : Γ × Γ') × Γ × Γ))
        ((VAddAntidiagonal (s := x.support + y.support) (t :=
              HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) b
              ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1)
        a →
      HSMul.hSMul (β := V)
          (x.coeff a.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ).1 * y.coeff a.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ).2)
          (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) 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 •
          HSMul.hSMul (β := V)
            (y.coeff
              (Sigma.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ')
                    (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
                    | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j)) :
                  Γ × Γ').1)
            (coeff.{u_2, u_5} (Γ := Γ') ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z : V⟦Γ'⟧)
              ((Sigma.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ')
                    (match (motive := (_ : Γ × Γ') × Γ × Γ → (_ : Γ × Γ') × Γ × Γ') a with
                    | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : Γ × Γ') ↦ Γ × Γ') (k, l +ᵥ j) (l, j))).2 :
                Γ'))
⊢ Eq.{u_5 + 1} (α := V)
    (∑
      x_1 ∈
        (VAddAntidiagonal (s := x.support + y.support) (t :=
              HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) b
              ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ) fun (a : Γ × Γ') ↦ addAntidiagonal (s := x.support) (t := y.support) ⋯ ⋯ a.1,
      HSMul.hSMul (β := V)
        (x.coeff x_1.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ).1 * y.coeff x_1.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ).2)
        (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) x_1.fst (β := fun (i : Γ × Γ') ↦ Γ × Γ).2))
    (∑
      x_1 ∈
        (VAddAntidiagonal (s := x.support) (t :=
              HVAdd.hVAdd (β := Set Γ') y.support
                (HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)))
              b ⋯).sigma
          (α := fun (a : Γ × Γ') ↦ Γ × Γ') fun (a : Γ × Γ') ↦
          VAddAntidiagonal (s := y.support) (t :=
            HahnSeries.support.{u_2, u_5} (R := V) ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z)) a.2 ⋯,
      x.coeff x_1.fst (β := fun (i : Γ × Γ') ↦ Γ × Γ').1 •
        HSMul.hSMul (β := V) (y.coeff x_1.snd (β := fun (i : Γ × Γ') ↦ Γ × Γ').1)
          (coeff ((Equiv.symm (of R) : (a : HahnModule Γ' R V) → V⟦Γ'⟧) z) 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'