-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.Inverse (goal)
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
neg :
  ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    Membership.mem (α := (Unit →₀ ℕ) × (Unit →₀ ℕ)) (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ)))
      (@antidiagonal _ Finsupp.instAddMonoid _ (single () n))
      (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
        | (a, b) => (single () a, single () b) :
        (Unit →₀ ℕ) × (Unit →₀ ℕ))
neg₁ :
  ∀ (a : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    Membership.mem (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ))) (@antidiagonal _ Finsupp.instAddMonoid _ (single () n)) a →
      Membership.mem (α := ℕ × ℕ) (@antidiagonal _ Nat.instAddMonoid _ n)
        (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ) a with
          | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ()) :
          ℕ × ℕ)
neg₂ :
  ∀ a ∈ @antidiagonal _ Nat.instAddMonoid _ n,
    (match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ)
        match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ())) =
      a
neg₃ :
  ∀ (a : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    Membership.mem (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ))) (@antidiagonal _ Finsupp.instAddMonoid _ (single () n)) a →
      (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ))
          match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ) a with
          | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ()) with
        | (a, b) => (single () a, single () b)) =
        a
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
      if x.2 < n then
        HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff x.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
    (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ (single () n),
      if x.2 < single () n then
        HMul.hMul (α := R) (β := R) ((MvPowerSeries.coeff x.1 : (a : MvPowerSeries Unit R) → R) φ : R)
          ((MvPowerSeries.coeff x.2 : (a : MvPowerSeries Unit R) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0)
have neg₄ : ∀ a_1 ∈ @antidiagonal _ Nat.instAddMonoid _ n,
  (if a_1.2 < n then
      HMul.hMul (α := R) (β := R) ((coeff a_1.1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff a_1.2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a_1 with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a_1 with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) a_1 with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0
Tactic: apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b))
    fun (f, g) ↦ (f (), g ())