-- Mathlib/RingTheory/MvPowerSeries/Inverse.lean
theorem mul_invOfUnit (φ : MvPowerSeries σ R) (u : Rˣ) (h : constantCoeff σ R φ = u) :
    φ * invOfUnit φ u = 1 :=
  ext fun n =>
    letI := Classical.decEq (σ →₀ ℕ)
    if H : n = 0 then by
      rw [H]
      simp [coeff_mul, support_single_ne_zero, h]
    else by
      classical
      have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n

Proof state:
case mk.intro.hc.bc.right.h
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H✝ : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
H : i ≤ 0
s : σ
⊢ i s = 0 s

Tactic:
exact Nat.eq_zero_of_le_zero (H s)

Result:
no goals

Proof state:
case mk.intro.hc.bc.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
s : σ
⊢ 0 s ≤ i s

Tactic:
exact Nat.zero_le _

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
⊢ (0, n) ∈ antidiagonal n

Tactic:
rw [mem_antidiagonal, zero_add]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ (coeff R n) (φ * φ.invOfUnit u) = (coeff R n) 1

Tactic:
rw [coeff_one, if_neg H, coeff_mul, ← Finset.insert_erase this,
  Finset.sum_insert (Finset.not_mem_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.not_mem_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]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ∀ x ∈ (antidiagonal n).erase (0, n),
    (coeff R x.1) φ * (coeff R x.2) (φ.invOfUnit u) =
      if x.2 < (0, n).2 then (coeff R x.1) φ * (coeff R x.2) (φ.invOfUnit u) else 0

Proof state:
case mk.intro.hc.bc.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
⊢ 0 ≤ i

Tactic:
intro s

Result:
case mk.intro.hc.bc.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
s : σ
⊢ 0 s ≤ i s

Proof state:
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H✝ : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
H : i ≤ 0
⊢ False

Tactic:
apply h₁

Result:
case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H✝ : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
H : i ≤ 0
⊢ (i, j) = (0, (i, j).1 + (i, j).2)

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
⊢ (coeff R n) (φ * φ.invOfUnit u) = (coeff R n) 1

Tactic:
have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add]

Result:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ (coeff R n) (φ * φ.invOfUnit u) = (coeff R n) 1

Proof state:
case mk.intro.hc.bc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
⊢ 0 < i

Tactic:
constructor

Result:
case mk.intro.hc.bc.left
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
⊢ 0 ≤ i

case mk.intro.hc.bc.right
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
⊢ ¬i ≤ 0

Proof state:
case mk.intro.hc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
⊢ 0 + j < i + j

Tactic:
apply add_lt_add_right

Result:
case mk.intro.hc.bc
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
i j : σ →₀ ℕ
H : ¬(i, j).1 + (i, j).2 = 0
this : (0, (i, j).1 + (i, j).2) ∈ antidiagonal ((i, j).1 + (i, j).2)
h₁ : (i, j) ≠ (0, (i, j).1 + (i, j).2)
⊢ 0 < i

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
⊢ ∀ x ∈ (antidiagonal n).erase (0, n),
    (coeff R x.1) φ * (coeff R x.2) (φ.invOfUnit u) =
      if x.2 < (0, n).2 then (coeff R x.1) φ * (coeff R x.2) (φ.invOfUnit u) else 0

Tactic:
rintro ⟨i, j⟩ hij

Result:
case mk
σ : Type u_1
R : Type u_2
inst✝ : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff σ R) φ = ↑u
n : σ →₀ ℕ
this✝ : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (0, n) ∈ antidiagonal n
i j : σ →₀ ℕ
hij : (i, j) ∈ (antidiagonal n).erase (0, n)
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) =
    if (i, j).2 < (0, n).2 then (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) else 0