-- Module: Mathlib.RingTheory.PowerSeries.Inverse
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
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
⊢ 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)

Tactic:
apply Finset.sum_nbij' (fun (a, b) ↦ (single () a, single () b))
    fun (f, g) ↦ (f (), g ())

Premises used: Finset.sum_nbij'