-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem coeff_inv_aux (n : ℕ) (a : R) (φ : R⟦X⟧) :
    coeff R n (inv.aux a φ) =
      if n = 0 then a
      else
        -a *
          ∑ x ∈ antidiagonal n,
            if x.2 < n then coeff R x.1 φ * coeff R x.2 (inv.aux a φ) else 0

Proof state:
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (coeff R n) (inv.aux a φ) =
    if n = 0 then a else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (inv.aux a φ) else 0

Tactic:
rw [coeff, inv.aux, MvPowerSeries.coeff_inv_aux]

Result:
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
⊢ (if single () n = 0 then a
    else
      -a *
        ∑ x ∈ antidiagonal (single () n),
          if x.2 < single () n then
            (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (MvPowerSeries.inv.aux a φ)
          else 0) =
    if n = 0 then a
    else -a * ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0

Proof state:
case neg.e_a.h.mk.inr.hc.refine_1.unit
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
        | (a, b) => (single () a, single () b)).2
      PUnit.unit ≤
    (single () n) PUnit.unit

Tactic:
simpa [Finsupp.single_eq_same] using le_of_lt H

Result:
no goals

Proof state:
case neg.e_a.hj
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal (single () n),
    (match a with
      | (f, g) => (f (), g ())) ∈
      antidiagonal n

Tactic:
aesop

Result:
no goals

Proof state:
case neg.e_a.hi
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match a with
      | (a, b) => (single () a, single () b)) ∈
      antidiagonal (single () n)

Tactic:
aesop

Result:
no goals

Proof state:
case neg.e_a.left_inv
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a ∈ antidiagonal n,
    (match
        match a with
        | (a, b) => (single () a, single () b) with
      | (f, g) => (f (), g ())) =
      a

Tactic:
aesop

Result:
no goals

Proof state:
case neg.e_a.h.mk.inr.hc
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
      | (a, b) => (single () a, single () b)).2 <
    single () n

Tactic:
refine ⟨?_, fun hh ↦ H.not_le ?_⟩

Result:
case neg.e_a.h.mk.inr.hc.refine_1
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (match (i, j) with
      | (a, b) => (single () a, single () b)).2 ≤
    single () n

case neg.e_a.h.mk.inr.hc.refine_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j

Proof state:
case neg.e_a.h
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ ∀ a_1 ∈ antidiagonal n,
    (if a_1.2 < n then (coeff R a_1.1) φ * (coeff R a_1.2) (MvPowerSeries.inv.aux a φ) else 0) =
      if
          (match a_1 with
              | (a, b) => (single () a, single () b)).2 <
            single () n then
        (MvPowerSeries.coeff R
              (match a_1 with
                | (a, b) => (single () a, single () b)).1)
            φ *
          (MvPowerSeries.coeff R
              (match a_1 with
                | (a, b) => (single () a, single () b)).2)
            (MvPowerSeries.inv.aux a φ)
      else 0

Tactic:
rintro ⟨i, j⟩ _hij

Result:
case neg.e_a.h.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
⊢ (if (i, j).2 < n then (coeff R (i, j).1) φ * (coeff R (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff R
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff R
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0

Proof state:
case neg.e_a
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ (∑ x ∈ antidiagonal (single () n),
      if x.2 < single () n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (MvPowerSeries.inv.aux a φ)
      else 0) =
    ∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0

Tactic:
symm

Result:
case neg.e_a
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
⊢ (∑ x ∈ antidiagonal n, if x.2 < n then (coeff R x.1) φ * (coeff R x.2) (MvPowerSeries.inv.aux a φ) else 0) =
    ∑ x ∈ antidiagonal (single () n),
      if x.2 < single () n then (MvPowerSeries.coeff R x.1) φ * (MvPowerSeries.coeff R x.2) (MvPowerSeries.inv.aux a φ)
      else 0

Proof state:
case neg.e_a.h.mk.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) (MvPowerSeries.inv.aux a φ) =
    (MvPowerSeries.coeff R
          (match (i, j) with
            | (a, b) => (single () a, single () b)).1)
        φ *
      (MvPowerSeries.coeff R
          (match (i, j) with
            | (a, b) => (single () a, single () b)).2)
        (MvPowerSeries.inv.aux a φ)

Tactic:
rfl

Result:
no goals

Proof state:
case neg.e_a.h.mk
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
⊢ (if (i, j).2 < n then (coeff R (i, j).1) φ * (coeff R (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff R
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff R
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0

Tactic:
obtain H | H := le_or_lt n j

Result:
case neg.e_a.h.mk.inl
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : n ≤ j
⊢ (if (i, j).2 < n then (coeff R (i, j).1) φ * (coeff R (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff R
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff R
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0

case neg.e_a.h.mk.inr
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
⊢ (if (i, j).2 < n then (coeff R (i, j).1) φ * (coeff R (i, j).2) (MvPowerSeries.inv.aux a φ) else 0) =
    if
        (match (i, j) with
            | (a, b) => (single () a, single () b)).2 <
          single () n then
      (MvPowerSeries.coeff R
            (match (i, j) with
              | (a, b) => (single () a, single () b)).1)
          φ *
        (MvPowerSeries.coeff R
            (match (i, j) with
              | (a, b) => (single () a, single () b)).2)
          (MvPowerSeries.inv.aux a φ)
    else 0

Proof state:
case neg.e_a.h.mk.inr.hc.refine_2
R : Type u_1
inst✝ : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h✝ : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ antidiagonal n
H : j < n
hh :
  single () n ≤
    (match (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j

Tactic:
simpa [Finsupp.single_eq_same] using hh ()

Result:
no goals