R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
⊢ (if single () n = 0 then a
    else
      -a *
        ∑ x in Finsupp.antidiagonal (single () n),
          if x.snd < single () n then
            ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x in Finset.Nat.antidiagonal n,
          if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
⊢ ↑(coeff R n) (inv.aux a φ) =
    if n = 0 then a
    else
      -a *
        ∑ x in Finset.Nat.antidiagonal n, if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (inv.aux a φ) else 0
rw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux]
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
⊢ (if n = 0 then a
    else
      -a *
        ∑ x in Finsupp.antidiagonal (single () n),
          if x.snd < single () n then
            ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x in Finset.Nat.antidiagonal n,
          if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
⊢ (if single () n = 0 then a
    else
      -a *
        ∑ x in Finsupp.antidiagonal (single () n),
          if x.snd < single () n then
            ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x in Finset.Nat.antidiagonal n,
          if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0
simp only [Finsupp.single_eq_zero]
case inl
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : n = 0
⊢ a = a

case inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ (-a *
      ∑ x in Finsupp.antidiagonal (single () n),
        if x.snd < single () n then
          ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
        else 0) =
    -a *
      ∑ x in Finset.Nat.antidiagonal n,
        if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
⊢ (if n = 0 then a
    else
      -a *
        ∑ x in Finsupp.antidiagonal (single () n),
          if x.snd < single () n then
            ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
          else 0) =
    if n = 0 then a
    else
      -a *
        ∑ x in Finset.Nat.antidiagonal n,
          if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0
split_ifs
case inr.e_a
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ (∑ x in Finsupp.antidiagonal (single () n),
      if x.snd < single () n then
        ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
      else 0) =
    ∑ x in Finset.Nat.antidiagonal n,
      if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0
case inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ (-a *
      ∑ x in Finsupp.antidiagonal (single () n),
        if x.snd < single () n then
          ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
        else 0) =
    -a *
      ∑ x in Finset.Nat.antidiagonal n,
        if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0
congr 1
case inr.e_a
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ (∑ x in Finset.Nat.antidiagonal n,
      if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0) =
    ∑ x in Finsupp.antidiagonal (single () n),
      if x.snd < single () n then
        ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
      else 0
case inr.e_a
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ (∑ x in Finsupp.antidiagonal (single () n),
      if x.snd < single () n then
        ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
      else 0) =
    ∑ x in Finset.Nat.antidiagonal n,
      if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0
symm
case inr.e_a.hi
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ ∀ (a : ℕ × ℕ), a ∈ Finset.Nat.antidiagonal n → (single () a.fst, single () a.snd) ∈ Finsupp.antidiagonal (single () n)

case inr.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ ∀ (a_1 : ℕ × ℕ),
    a_1 ∈ Finset.Nat.antidiagonal n →
      (if a_1.snd < n then ↑(coeff R a_1.fst) φ * ↑(coeff R a_1.snd) (MvPowerSeries.inv.aux a φ) else 0) =
        if (single () a_1.fst, single () a_1.snd).snd < single () n then
          ↑(MvPowerSeries.coeff R (single () a_1.fst, single () a_1.snd).fst) φ *
            ↑(MvPowerSeries.coeff R (single () a_1.fst, single () a_1.snd).snd) (MvPowerSeries.inv.aux a φ)
        else 0

case inr.e_a.i_inj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ ∀ (a₁ a₂ : ℕ × ℕ),
    a₁ ∈ Finset.Nat.antidiagonal n →
      a₂ ∈ Finset.Nat.antidiagonal n →
        (single () a₁.fst, single () a₁.snd) = (single () a₂.fst, single () a₂.snd) → a₁ = a₂

case inr.e_a.i_surj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ ∀ (b : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    b ∈ Finsupp.antidiagonal (single () n) → ∃ a ha, b = (single () a.fst, single () a.snd)
case inr.e_a
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ (∑ x in Finset.Nat.antidiagonal n,
      if x.snd < n then ↑(coeff R x.fst) φ * ↑(coeff R x.snd) (MvPowerSeries.inv.aux a φ) else 0) =
    ∑ x in Finsupp.antidiagonal (single () n),
      if x.snd < single () n then
        ↑(MvPowerSeries.coeff R x.fst) φ * ↑(MvPowerSeries.coeff R x.snd) (MvPowerSeries.inv.aux a φ)
      else 0
apply Finset.sum_bij fun (p : ℕ × ℕ) _h => (single () p.1, single () p.2)
no goals
case inl
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : n = 0
⊢ a = a
rfl
case inr.e_a.hi.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ (single () (i, j).fst, single () (i, j).snd) ∈ Finsupp.antidiagonal (single () n)
case inr.e_a.hi
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ ∀ (a : ℕ × ℕ), a ∈ Finset.Nat.antidiagonal n → (single () a.fst, single () a.snd) ∈ Finsupp.antidiagonal (single () n)
rintro ⟨i, j⟩ hij
case inr.e_a.hi.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
⊢ (single () (i, j).fst, single () (i, j).snd) ∈ Finsupp.antidiagonal (single () n)
case inr.e_a.hi.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ (single () (i, j).fst, single () (i, j).snd) ∈ Finsupp.antidiagonal (single () n)
rw [Finset.Nat.mem_antidiagonal] at hij
no goals
case inr.e_a.hi.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
hij : (i, j).fst + (i, j).snd = n
⊢ (single () (i, j).fst, single () (i, j).snd) ∈ Finsupp.antidiagonal (single () n)
rw [Finsupp.mem_antidiagonal, ← Finsupp.single_add, hij]
case inr.e_a.h.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ (if (i, j).snd < n then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (MvPowerSeries.inv.aux a φ) else 0) =
    if (single () (i, j).fst, single () (i, j).snd).snd < single () n then
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
        ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) (MvPowerSeries.inv.aux a φ)
    else 0
case inr.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ ∀ (a_1 : ℕ × ℕ),
    a_1 ∈ Finset.Nat.antidiagonal n →
      (if a_1.snd < n then ↑(coeff R a_1.fst) φ * ↑(coeff R a_1.snd) (MvPowerSeries.inv.aux a φ) else 0) =
        if (single () a_1.fst, single () a_1.snd).snd < single () n then
          ↑(MvPowerSeries.coeff R (single () a_1.fst, single () a_1.snd).fst) φ *
            ↑(MvPowerSeries.coeff R (single () a_1.fst, single () a_1.snd).snd) (MvPowerSeries.inv.aux a φ)
        else 0
rintro ⟨i, j⟩ _hij
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ (if (i, j).snd < n then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (MvPowerSeries.inv.aux a φ) else 0) =
    if (single () (i, j).fst, single () (i, j).snd).snd < single () n then
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
        ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) (MvPowerSeries.inv.aux a φ)
    else 0

case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
⊢ (if (i, j).snd < n then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (MvPowerSeries.inv.aux a φ) else 0) =
    if (single () (i, j).fst, single () (i, j).snd).snd < single () n then
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
        ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) (MvPowerSeries.inv.aux a φ)
    else 0
case inr.e_a.h.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
⊢ (if (i, j).snd < n then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (MvPowerSeries.inv.aux a φ) else 0) =
    if (single () (i, j).fst, single () (i, j).snd).snd < single () n then
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
        ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) (MvPowerSeries.inv.aux a φ)
    else 0
by_cases H : j < n
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (MvPowerSeries.inv.aux a φ) =
    ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) (MvPowerSeries.inv.aux a φ)

case pos.hc
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ (single () (i, j).fst, single () (i, j).snd).snd < single () n
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ (if (i, j).snd < n then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (MvPowerSeries.inv.aux a φ) else 0) =
    if (single () (i, j).fst, single () (i, j).snd).snd < single () n then
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
        ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) (MvPowerSeries.inv.aux a φ)
    else 0
rw [if_pos H, if_pos]
case pos.hc.left
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd i_1) (↑(single () n) i_1)

case pos.hc.right
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ ¬∀ (i_1 : Unit),
      PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
case pos.hc
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ (single () (i, j).fst, single () (i, j).snd).snd < single () n
constructor
no goals
case pos
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (MvPowerSeries.inv.aux a φ) =
    ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) (MvPowerSeries.inv.aux a φ)
rfl
case pos.hc.left.unit
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd PUnit.unit) (↑(single () n) PUnit.unit)
case pos.hc.left
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd i_1) (↑(single () n) i_1)
rintro ⟨⟩
no goals
case pos.hc.left.unit
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd PUnit.unit) (↑(single () n) PUnit.unit)
simpa [Finsupp.single_eq_same] using le_of_lt H
case pos.hc.right
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
hh :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ False
case pos.hc.right
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
⊢ ¬∀ (i_1 : Unit),
      PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
intro hh
case pos.hc.right
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j ≥ n
hh :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ False
case pos.hc.right
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : j < n
hh :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ False
rw [lt_iff_not_ge] at H
case pos.hc.right
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j ≥ n
hh :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ j ≥ n
case pos.hc.right
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j ≥ n
hh :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ False
apply H
no goals
case pos.hc.right
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j ≥ n
hh :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ j ≥ n
simpa [Finsupp.single_eq_same] using hh ()
case neg.hnc
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
⊢ ¬(single () (i, j).fst, single () (i, j).snd).snd < single () n
case neg
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
⊢ (if (i, j).snd < n then ↑(coeff R (i, j).fst) φ * ↑(coeff R (i, j).snd) (MvPowerSeries.inv.aux a φ) else 0) =
    if (single () (i, j).fst, single () (i, j).snd).snd < single () n then
      ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).fst) φ *
        ↑(MvPowerSeries.coeff R (single () (i, j).fst, single () (i, j).snd).snd) (MvPowerSeries.inv.aux a φ)
    else 0
rw [if_neg H, if_neg]
case neg.hnc.intro
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
_h₁ :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd i_1) (↑(single () n) i_1)
h₂ :
  ¬∀ (i_1 : Unit),
      PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ False
case neg.hnc
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
⊢ ¬(single () (i, j).fst, single () (i, j).snd).snd < single () n
rintro ⟨_h₁, h₂⟩
case neg.hnc.intro
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
_h₁ :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd i_1) (↑(single () n) i_1)
h₂ :
  ¬∀ (i_1 : Unit),
      PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
case neg.hnc.intro
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
_h₁ :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd i_1) (↑(single () n) i_1)
h₂ :
  ¬∀ (i_1 : Unit),
      PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ False
apply h₂
case neg.hnc.intro.unit
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
_h₁ :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd i_1) (↑(single () n) i_1)
h₂ :
  ¬∀ (i_1 : Unit),
      PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ PartialOrder.toPreorder.1.1 (↑(single () n) PUnit.unit) (↑(single () (i, j).fst, single () (i, j).snd).snd PUnit.unit)
case neg.hnc.intro
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
_h₁ :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd i_1) (↑(single () n) i_1)
h₂ :
  ¬∀ (i_1 : Unit),
      PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
rintro ⟨⟩
no goals
case neg.hnc.intro.unit
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
H : ¬j < n
_h₁ :
  ∀ (i_1 : Unit),
    PartialOrder.toPreorder.1.1 (↑(single () (i, j).fst, single () (i, j).snd).snd i_1) (↑(single () n) i_1)
h₂ :
  ¬∀ (i_1 : Unit),
      PartialOrder.toPreorder.1.1 (↑(single () n) i_1) (↑(single () (i, j).fst, single () (i, j).snd).snd i_1)
⊢ PartialOrder.toPreorder.1.1 (↑(single () n) PUnit.unit) (↑(single () (i, j).fst, single () (i, j).snd).snd PUnit.unit)
simpa [Finsupp.single_eq_same] using not_lt.1 H
case inr.e_a.i_inj.mk.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j k l : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
_hkl : (k, l) ∈ Finset.Nat.antidiagonal n
⊢ (single () (i, j).fst, single () (i, j).snd) = (single () (k, l).fst, single () (k, l).snd) → (i, j) = (k, l)
case inr.e_a.i_inj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ ∀ (a₁ a₂ : ℕ × ℕ),
    a₁ ∈ Finset.Nat.antidiagonal n →
      a₂ ∈ Finset.Nat.antidiagonal n →
        (single () a₁.fst, single () a₁.snd) = (single () a₂.fst, single () a₂.snd) → a₁ = a₂
rintro ⟨i, j⟩ ⟨k, l⟩ _hij _hkl
no goals
case inr.e_a.i_inj.mk.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
i j k l : ℕ
_hij : (i, j) ∈ Finset.Nat.antidiagonal n
_hkl : (k, l) ∈ Finset.Nat.antidiagonal n
⊢ (single () (i, j).fst, single () (i, j).snd) = (single () (k, l).fst, single () (k, l).snd) → (i, j) = (k, l)
simpa only [Prod.mk.inj_iff, Finsupp.unique_single_eq_iff] using id
case inr.e_a.i_surj.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ ∃ a ha, (f, g) = (single () a.fst, single () a.snd)
case inr.e_a.i_surj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
⊢ ∀ (b : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    b ∈ Finsupp.antidiagonal (single () n) → ∃ a ha, b = (single () a.fst, single () a.snd)
rintro ⟨f, g⟩ hfg
case inr.e_a.i_surj.mk.refine'_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ (↑f (), ↑g ()) ∈ Finset.Nat.antidiagonal n

case inr.e_a.i_surj.mk.refine'_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ (f, g) = (single () (↑f (), ↑g ()).fst, single () (↑f (), ↑g ()).snd)
case inr.e_a.i_surj.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ ∃ a ha, (f, g) = (single () a.fst, single () a.snd)
refine' ⟨(f (), g ()), _, _⟩
case inr.e_a.i_surj.mk.refine'_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g).fst + (f, g).snd = single () n
⊢ (↑f (), ↑g ()) ∈ Finset.Nat.antidiagonal n
case inr.e_a.i_surj.mk.refine'_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ (↑f (), ↑g ()) ∈ Finset.Nat.antidiagonal n
rw [Finsupp.mem_antidiagonal] at hfg
no goals
case inr.e_a.i_surj.mk.refine'_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g).fst + (f, g).snd = single () n
⊢ (↑f (), ↑g ()) ∈ Finset.Nat.antidiagonal n
rw [Finset.Nat.mem_antidiagonal, ← Finsupp.add_apply, hfg, Finsupp.single_eq_same]
case inr.e_a.i_surj.mk.refine'_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ f = single () (↑f (), ↑g ()).fst ∧ g = single () (↑f (), ↑g ()).snd
case inr.e_a.i_surj.mk.refine'_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ (f, g) = (single () (↑f (), ↑g ()).fst, single () (↑f (), ↑g ()).snd)
rw [Prod.mk.inj_iff]
case inr.e_a.i_surj.mk.refine'_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ f = single () (↑f ()) ∧ g = single () (↑g ())
case inr.e_a.i_surj.mk.refine'_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ f = single () (↑f (), ↑g ()).fst ∧ g = single () (↑f (), ↑g ()).snd
dsimp
no goals
case inr.e_a.i_surj.mk.refine'_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : PowerSeries R
h✝ : ¬n = 0
f g : Unit →₀ ℕ
hfg : (f, g) ∈ Finsupp.antidiagonal (single () n)
⊢ f = single () (↑f ()) ∧ g = single () (↑g ())
exact ⟨Finsupp.unique_single f, Finsupp.unique_single g⟩