-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
neg :
  ∀ (H : n ≤ j),
    (if (i, j).2 < n then
        HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0) =
      if
          LT.lt (α := Unit →₀ ℕ)
            (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
              | (a, b) => (single () a, single () b)).2
            (single () n) then
        HMul.hMul (α := R) (β := R)
          ((MvPowerSeries.coeff
                  (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                    | (a, b) => (single () a, single () b)).1 :
                (a : MvPowerSeries Unit R) → R)
              φ :
            R)
          ((MvPowerSeries.coeff
                  (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                    | (a, b) => (single () a, single () b)).2 :
                (a : MvPowerSeries Unit R) → R)
              (MvPowerSeries.inv.aux a φ) :
            R)
      else 0
neg₁ :
  ∀ (H : j < n),
    (if (i, j).2 < n then
        HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
          ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
      else 0) =
      if
          LT.lt (α := Unit →₀ ℕ)
            (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
              | (a, b) => (single () a, single () b)).2
            (single () n) then
        HMul.hMul (α := R) (β := R)
          ((MvPowerSeries.coeff
                  (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                    | (a, b) => (single () a, single () b)).1 :
                (a : MvPowerSeries Unit R) → R)
              φ :
            R)
          ((MvPowerSeries.coeff
                  (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                    | (a, b) => (single () a, single () b)).2 :
                (a : MvPowerSeries Unit R) → R)
              (MvPowerSeries.inv.aux a φ) :
            R)
      else 0
⊢ (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0

Tactic:
obtain H | H := le_or_gt n j

Premises used: le_or_gt