awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
inst_1 : DecidableEq σ
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ inv.aux a φ n =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
          else 0
have refl : inv.aux a φ n =
  if n = 0 then a
  else
    -a *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        if x.2 < n then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
        else 0
Tactic: cases Subsingleton.elim ‹DecidableEq σ› (Classical.decEq σ)
Cleared hypotheses: inst_1
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
n : σ →₀ ℕ
a : R
φ : MvPowerSeries σ R
⊢ inv.aux a φ n =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
              ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
          else 0
have refl : (if n = 0 then a
  else
    -a *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        if x_1 : x.2 < n then HMul.hMul (α := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R) (inv.aux a φ x.2)
        else 0) =
  if n = 0 then a
  else
    -a *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
        if x.2 < n then
          HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : MvPowerSeries σ R) → R) φ : R)
            ((coeff x.2 : (a : MvPowerSeries σ R) → R) (inv.aux a φ) : R)
        else 0
Tactic: rw [inv.aux]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw : (coeff 0 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
rw : (coeff 0 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw₁ : (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then (↑u⁻¹ : R)
  else
    -(↑u⁻¹ : R) *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
        if x.2 < 0 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) =
  (↑u⁻¹ : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
rw : (coeff 0 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
rw₁ :
  (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
          if x.2 < 0 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) =
    (↑u⁻¹ : R)
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw₂ : (↑u⁻¹ : R) = (↑u⁻¹ : R)
Tactic: rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw : (coeff 0 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
Tactic: classical
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
rw : (coeff 0 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw₁ : (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then (↑u⁻¹ : R)
  else
    -(↑u⁻¹ : R) *
      ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
        if x.2 < 0 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) =
  (↑u⁻¹ : R)
Tactic: classical
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
rw : (coeff 0 : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
rw₁ :
  (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
          if x.2 < 0 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) =
    (↑u⁻¹ : R)
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
have rw₂ : (↑u⁻¹ : R) = (↑u⁻¹ : R)
Tactic: classical
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_invOfUnit, if_pos rfl]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
have rw : Eq.{u_2 + 1} (α := R) ((coeff 0 : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
  ((coeff 0 : (a : MvPowerSeries σ R) → R) 1 : R)
Tactic: rw [H]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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
⊢ (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
have rw : (0, n).1 + (0, n).2 = n
Tactic: rw [mem_antidiagonal, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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
rw : (0, n).1 + (0, n).2 = n
⊢ (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
have rw₁ : (0, n).2 = n
Tactic: rw [mem_antidiagonal, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (hypothesis)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
have this₁ : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
Tactic: have : ((0 : σ →₀ ℕ), n) ∈ antidiagonal n := by rw [mem_antidiagonal, zero_add]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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_1 : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
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 rw : ∀ 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
Tactic: 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]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (hypothesis)
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_1 : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
this : (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 hij₁ : (i, j) ≠ (0, n) ∧ (i, j).1 + (i, j).2 = n
Tactic: rw [Finset.mem_erase, mem_antidiagonal] at hij
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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_1 : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
H : ¬n = 0
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 obtain : ∀ (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
Tactic: obtain ⟨h₁, rfl⟩ := hij
Cleared hypotheses: n, H, this, hij
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
this_1 : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
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
have hc : (i, j).2 < (0, (i, j).1 + (i, j).2).2
Tactic: rw [if_pos]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
this_1 : DecidableEq (σ →₀ ℕ) := Classical.decEq (σ →₀ ℕ)
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
have hc : (i, j).1 ≠ 0
Tactic: refine lt_add_of_pos_left _ <| pos_iff_ne_zero.2 ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
have have : (0, n) ∈ @antidiagonal _ Finsupp.instAddMonoid _ n
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₁
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
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)
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₁
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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)
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
have 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
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₁
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
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
⊢ Eq.{u_2 + 1} (α := R) ((coeff n : (a : MvPowerSeries σ R) → R) (φ * φ.invOfUnit u) : R)
    ((coeff n : (a : MvPowerSeries σ R) → R) 1 : R)
have 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
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₁
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
⊢ φ.invOfUnit u * φ = 1
have rw : Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisors (MvPowerSeries σ R)) (φ.invOfUnit u)
Tactic: rw [← mul_cancel_right_mem_nonZeroDivisors (r := φ.invOfUnit u), mul_assoc, one_mul,
    mul_invOfUnit _ _ h, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisors (MvPowerSeries σ R)) (φ.invOfUnit u)
have hφ : Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisors R)
  ((constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
Tactic: apply mem_nonZeroDivisors_of_constantCoeff
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
⊢ IsUnit φ ↔ IsUnit.{u_2} (M := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
have mp : IsUnit φ → IsUnit.{u_2} (M := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
mp : IsUnit φ → IsUnit.{u_2} (M := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
⊢ IsUnit φ ↔ IsUnit.{u_2} (M := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
have mpr : IsUnit.{u_2} (M := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) → IsUnit φ
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
φ : MvPowerSeries σ R
⊢ IsUnit φ ∨ IsUnit (1 - φ)
have inl : ∀ (u : Rˣ) (h : (↑u : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ), IsUnit φ ∨ IsUnit (1 - φ)
Tactic: obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
φ : MvPowerSeries σ R
inl : ∀ (u : Rˣ) (h : (↑u : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ), IsUnit φ ∨ IsUnit (1 - φ)
⊢ IsUnit φ ∨ IsUnit (1 - φ)
have inr : ∀ (u : Rˣ) (h : (↑u : R) = HSub.hSub (α := R) (β := R) (1 : R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)),
  IsUnit φ ∨ IsUnit (1 - φ)
Tactic: obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ)
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : (↑u : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ
⊢ IsUnit φ ∨ IsUnit (1 - φ)
have inl : IsUnit φ
Tactic: left
-- Lean 4 proof step from Mathlib.RingTheory.MvPowerSeries.Inverse (goal)
Goal:
σ : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsLocalRing R
φ : MvPowerSeries σ R
u : Rˣ
h : (↑u : R) = HSub.hSub (α := R) (β := R) (1 : R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)
⊢ IsUnit φ ∨ IsUnit (1 - φ)
have inr : IsUnit (1 - φ)
Tactic: right