-- 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
σ : 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

Tactic:
intro 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
⊢ False

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
⊢ i = 0

Tactic:
ext1 s

Result:
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

Proof state:
case mk.intro
σ : 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)
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) =
    if (i, j).2 < (0, (i, j).1 + (i, j).2).2 then (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) else 0

Tactic:
rw [if_pos]

Result:
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)
⊢ (i, j).2 < (0, (i, j).1 + (i, j).2).2

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)
⊢ (i, j).2 < (0, (i, j).1 + (i, j).2).2

Tactic:
suffices 0 + j < i + j by simpa

Result:
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

Proof state:
case mk.intro
σ : 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 : σ →₀ ℕ
h₁ : (i, j) ≠ (0, n)
h₂ : (i, j).1 + (i, j).2 = 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

Tactic:
subst n

Result:
case mk.intro
σ : 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)
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) =
    if (i, j).2 < (0, (i, j).1 + (i, j).2).2 then (coeff R (i, j).1) φ * (coeff R (i, j).2) (φ.invOfUnit u) else 0

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
⊢ (i, j) = (0, (i, j).1 + (i, j).2)

Tactic:
suffices i = 0 by simp [this]

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 = 0

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:
rw [H]

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
⊢ (coeff R 0) (φ * φ.invOfUnit u) = (coeff R 0) 1

Proof state:
σ : 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)
this : 0 + j < i + j
⊢ (i, j).2 < (0, (i, j).1 + (i, j).2).2

Tactic:
simpa

Result:
no goals

Proof state:
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) ≠ (0, n) ∧ (i, j).1 + (i, j).2 = 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

Tactic:
obtain ⟨h₁, h₂⟩ := hij

Result:
case mk.intro
σ : 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 : σ →₀ ℕ
h₁ : (i, j) ≠ (0, n)
h₂ : (i, j).1 + (i, j).2 = 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

Proof state:
σ : 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
this : i = 0
⊢ (i, j) = (0, (i, j).1 + (i, j).2)

Tactic:
simp [this]

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
⊢ (coeff R 0) (φ * φ.invOfUnit u) = (coeff R 0) 1

Tactic:
simp [coeff_mul, support_single_ne_zero, h]

Result:
no goals