-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
have : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
have₁ :
  ∀ (this : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
have₂ : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
have₃ have₄ :
  ∀ (this : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n),
    Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
      ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
have₅ :
  ∀ (this_1 : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n),
    ∀ x ∈ (@antidiagonal _ Finsupp.instAddMonoid _ n).erase (0, n),
      HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff x.2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R) =
        if x.2 < (0, n).2 then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
        else 0
have₆ :
  ∀ (this_1 : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n) (i j : σ →₀ ℕ)
    (hij : (i, j) ∈ (@antidiagonal _ Finsupp.instAddMonoid _ n).erase (0, n)),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R) =
      if (i, j).2 < (0, n).2 then
        HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
      else 0
have₇ :
  ∀ (this : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n) (i j : σ →₀ ℕ)
    (hij : (i, j) ≠ (0, n) ∧ (i, j).1 + (i, j).2 = n),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R) =
      if (i, j).2 < (0, n).2 then
        HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
      else 0
have₈ :
  ∀ (i j : σ →₀ ℕ) (H : ¬(i, j).1 + (i, j).2 = 0)
    (this : (0, (i, j).1 + (i, j).2) ∈ @antidiagonal _ Finsupp.instAddMonoid _ ((i, j).1 + (i, j).2))
    (h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)),
    HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
        ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R) =
      if (i, j).2 < (0, (i, j).1 + (i, j).2).2 then
        HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : MvPowerSeries σ R) → R) φ : R)
          ((coeff (i, j).2 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
      else 0
hc :
  ∀ (i j : σ →₀ ℕ) (H : ¬(i, j).1 + (i, j).2 = 0)
    (this : (0, (i, j).1 + (i, j).2) ∈ @antidiagonal _ Finsupp.instAddMonoid _ ((i, j).1 + (i, j).2))
    (h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)), (i, j).2 < (0, (i, j).1 + (i, j).2).2
hc₁ :
  ∀ (i j : σ →₀ ℕ) (H : ¬(i, j).1 + (i, j).2 = 0)
    (this : (0, (i, j).1 + (i, j).2) ∈ @antidiagonal _ Finsupp.instAddMonoid _ ((i, j).1 + (i, j).2))
    (h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)), (i, j).1 ≠ 0
hc₂ :
  ∀ (j : σ →₀ ℕ) (H : ¬(0, j).1 + (0, j).2 = 0)
    (this : (0, (0, j).1 + (0, j).2) ∈ @antidiagonal _ Finsupp.instAddMonoid _ ((0, j).1 + (0, j).2))
    (h₁ : Ne (α := (σ →₀ ℕ) × (σ →₀ ℕ)) (0, j) (0, (0, j).1 + (0, j).2)), False
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)

Tactic:
classical
      have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add]
      rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this,
        Finset.sum_insert (Finset.notMem_erase _ _), coeff_zero_eq_constantCoeff_apply, h,
        coeff_invOfUnit, if_neg H, neg_mul, mul_neg, Units.mul_inv_cancel_left, ←
        Finset.insert_erase this, Finset.sum_insert (Finset.notMem_erase _ _),
        Finset.insert_erase this, if_neg (not_lt_of_ge <| le_rfl), zero_add, add_comm, ←
        sub_eq_add_neg, sub_eq_zero, Finset.sum_congr rfl]
      rintro ⟨i, j⟩ hij
      rw [Finset.mem_erase, mem_antidiagonal] at hij
      obtain ⟨h₁, rfl⟩ := hij
      rw [if_pos]
      refine lt_add_of_pos_left _ <| pos_iff_ne_zero.2 ?_
      rintro rfl
      simp at h₁

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, Iff.mpr, le_rfl, sub_eq_zero, sub_eq_add_neg, MvPowerSeries.coeff_one, if_pos, zero_add, add_comm, Units.mul_inv_cancel_left, Finset.mem_erase, Finset.HasAntidiagonal.mem_antidiagonal, MvPowerSeries.coeff_invOfUnit, lt_add_of_pos_left, neg_mul, Finset.notMem_erase, Finset.sum_insert, pos_iff_ne_zero, if_neg, Finset.sum_congr, rfl, mul_neg, MvPowerSeries.coeff_mul, not_lt_of_ge