-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Basic (goal)
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) :
          (_ : (σ →₀ ℕ) × (σ →₀ ℕ)) × (σ →₀ ℕ) × (σ →₀ ℕ))
⊢ 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)))
have 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
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)⟩)