-- Module: Mathlib.RingTheory.MvPowerSeries.Basic
Goal:
σ : Type u_1
R : Type u_2
inst : Semiring R
φ₁ φ₂ φ₃ : MvPowerSeries σ R
n : σ →₀ ℕ
h :
  ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    Membership.mem (γ := Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1)
        a →
      Membership.mem (α := (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) (γ :=
        Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2)
        (match (motive :=
            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) → (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) a with
          | ⟨(_i, j), (k, l)⟩ => Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j) :
          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
h₁ :
  ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    Membership.mem (γ := Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2)
        a →
      Membership.mem (α := (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) (γ :=
        Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1)
        (match (motive :=
            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) → (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)) a with
          | ⟨(i, _j), (k, l)⟩ => Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (i + k, l) (i, k) :
          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
h₂ :
  ∀ (a : (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)),
    Membership.mem (γ := Finset ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ 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 ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ 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 ((_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ)))
        ((@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1)
        a →
      HMul.hMul (β := R)
          (HMul.hMul (α := R) (β := R)
            ((coeff a.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R)
                φ₁ :
              R)
            ((coeff a.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R)
                φ₂ :
              R))
          ((coeff a.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ :
            R) =
        HMul.hMul (α := R)
          ((coeff
                  (Sigma.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
                      (match (motive :=
                        (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) →
                          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
                        a with
                      | ⟨(_i, j), (k, l)⟩ =>
                        Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j))).1 :
                (a : MvPowerSeries σ R) → R)
              φ₁ :
            R)
          (HMul.hMul (α := R) (β := R)
            ((coeff
                    (Sigma.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
                        (match (motive :=
                          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) →
                            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
                          a with
                        | ⟨(_i, j), (k, l)⟩ =>
                          Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j))).1 :
                  (a : MvPowerSeries σ R) → R)
                φ₂ :
              R)
            ((coeff
                    (Sigma.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
                        (match (motive :=
                          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ) →
                            (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
                          a with
                        | ⟨(_i, j), (k, l)⟩ =>
                          Sigma.mk (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)) (k, l + j) (l, j))).2 :
                  (a : MvPowerSeries σ R) → R)
                φ₃ :
              R))
⊢ Eq.{u_2 + 1} (α := R)
    (∑
      x ∈
        (@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.1,
      HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R)
          ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₁ :
            R)
          ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₂ :
            R))
        ((coeff x.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ :
          R))
    (∑
      x ∈
        (@antidiagonal _ Finsupp.instAddMonoid _ n).sigma (α := fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ))
          fun (a : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ @antidiagonal _ Finsupp.instAddMonoid _ a.2,
      HMul.hMul (α := R)
        ((coeff x.fst (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₁ :
          R)
        (HMul.hMul (α := R) (β := R)
          ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).1 : (a : MvPowerSeries σ R) → R) φ₂ :
            R)
          ((coeff x.snd (β := fun (i : (σ →₀ ℕ) × (σ →₀ ℕ)) ↦ (σ →₀ ℕ) × (σ →₀ ℕ)).2 : (a : MvPowerSeries σ R) → R) φ₃ :
            R)))

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'