awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
hc : (i, j).2 < (0, (i, j).1 + (i, j).2).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:
rw [if_pos]

Premises used: if_pos
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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

Tactic:
lt_add_of_pos_left _ <| pos_iff_ne_zero.2 ?_

Premises used: Iff.mpr, lt_add_of_pos_left, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
hc : (i, j).1 ≠ 0
⊢ (i, j).2 < (0, (i, j).1 + (i, j).2).2

Tactic:
refine lt_add_of_pos_left _ <| pos_iff_ne_zero.2 ?_

Premises used: Iff.mpr, lt_add_of_pos_left, pos_iff_ne_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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 (σ →₀ ℕ)
j : σ →₀ ℕ
H : ¬(0, j).1 + (0, j).2 = 0
this : (0, (0, j).1 + (0, j).2) ∈ @antidiagonal _ Finsupp.instAddMonoid _ ((0, j).1 + (0, j).2)
h₁ : Ne (α := (σ →₀ ℕ) × (σ →₀ ℕ)) (0, j) (0, (0, j).1 + (0, j).2)
⊢ False

Tactic:
simp at h₁
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
rw : Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisors (MvPowerSeries σ R)) (φ.invOfUnit u)
⊢ φ.invOfUnit u * φ = 1

Tactic:
rw [← mul_cancel_right_mem_nonZeroDivisors (r := φ.invOfUnit u), mul_assoc, one_mul,
    mul_invOfUnit _ _ h, mul_one]

Premises used: mul_cancel_right_mem_nonZeroDivisors, mul_assoc, MvPowerSeries.mul_invOfUnit, mul_one, one_mul
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
h : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
hφ :
  Membership.mem (α := R) (γ := Submonoid R) (nonZeroDivisors R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)
⊢ Membership.mem (γ := Submonoid (MvPowerSeries σ R)) (nonZeroDivisors (MvPowerSeries σ R)) (φ.invOfUnit u)

Tactic:
apply mem_nonZeroDivisors_of_constantCoeff

Premises used: MvPowerSeries.mem_nonZeroDivisors_of_constantCoeff
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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 (α := R) (γ := Submonoid R) (nonZeroDivisors R)
    ((constantCoeff : (a : MvPowerSeries σ R) → R) (φ.invOfUnit u) : R)

Tactic:
simp only [constantCoeff_invOfUnit, IsUnit.mem_nonZeroDivisors (Units.isUnit u⁻¹)]

Premises used: MvPowerSeries.constantCoeff_invOfUnit, Inv.inv, IsUnit.mem_nonZeroDivisors, Units.isUnit
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
mpr : IsUnit.{u_2} (M := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) → IsUnit φ
⊢ IsUnit φ ↔ IsUnit.{u_2} (M := R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)

Tactic:
constructor
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)

Tactic:
IsUnit.map _

Premises used: IsUnit.map
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)

Tactic:
exact IsUnit.map _

Premises used: IsUnit.map
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
hu : (↑u : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ
⊢ IsUnit φ

Tactic:
⟨⟨_, φ.invOfUnit u, mul_invOfUnit φ u hu.symm, invOfUnit_mul φ u hu.symm⟩, rfl⟩

Premises used: IsUnit, MvPowerSeries.invOfUnit_mul, MvPowerSeries.invOfUnit, Units.mk, Exists.intro, MvPowerSeries.mul_invOfUnit, Eq.symm, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
inst : Ring R
φ : MvPowerSeries σ R
u : Rˣ
hu : (↑u : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ
⊢ IsUnit φ

Tactic:
exact ⟨⟨_, φ.invOfUnit u, mul_invOfUnit φ u hu.symm, invOfUnit_mul φ u hu.symm⟩, rfl⟩
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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 - φ)
inr :
  ∀ (u : Rˣ) (h : (↑u : R) = HSub.hSub (α := R) (β := R) (1 : R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)),
    IsUnit φ ∨ IsUnit (1 - φ)
⊢ IsUnit φ ∨ IsUnit (1 - φ)

Tactic:
obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ)

Premises used: IsLocalRing.isUnit_or_isUnit_one_sub_self, MvPowerSeries.constantCoeff, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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) φ
inl : IsUnit φ
⊢ IsUnit φ ∨ IsUnit (1 - φ)

Tactic:
left
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
inr : IsUnit (1 - φ)
⊢ IsUnit φ ∨ IsUnit (1 - φ)

Tactic:
right
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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 φ
inr :
  ∀ (u : Rˣ) (h : (↑u : R) = HSub.hSub (α := R) (β := R) (1 : R) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R)),
    IsUnit (1 - φ)
⊢ IsUnit φ ∨ IsUnit (1 - φ)

Tactic:
obtain ⟨u, h⟩ | ⟨u, h⟩ := IsLocalRing.isUnit_or_isUnit_one_sub_self (constantCoeff φ) <;>
        [left; right]

Premises used: IsLocalRing.isUnit_or_isUnit_one_sub_self, MvPowerSeries.constantCoeff, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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 φ

Tactic:
.of_mul_eq_one _ (mul_invOfUnit _ u ?_)

Premises used: IsUnit.of_mul_eq_one, MvPowerSeries.mul_invOfUnit
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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) φ
inl : (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)
⊢ IsUnit φ

Tactic:
refine .of_mul_eq_one _ (mul_invOfUnit _ u ?_)
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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) φ
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) φ = (↑u : R)

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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 (1 - φ)

Tactic:
.of_mul_eq_one _ (mul_invOfUnit _ u ?_)

Premises used: IsUnit.of_mul_eq_one, MvPowerSeries.mul_invOfUnit
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
inr : (constantCoeff : (a : MvPowerSeries σ R) → R) (1 - φ) = (↑u : R)
⊢ IsUnit (1 - φ)

Tactic:
refine .of_mul_eq_one _ (mul_invOfUnit _ u ?_)
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
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)
⊢ (constantCoeff : (a : MvPowerSeries σ R) → R) (1 - φ) = (↑u : R)

Tactic:
simpa using h.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h : (↑ψ : MvPowerSeries σ S) = (map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ
⊢ Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((constantCoeff : (a : MvPowerSeries σ S) → S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
      S)

Tactic:
replace h := congr_arg constantCoeff h
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((constantCoeff : (a : MvPowerSeries σ S) → S)
        ((map f : (a : MvPowerSeries σ R) → MvPowerSeries σ S) φ : MvPowerSeries σ S) :
      S)
⊢ Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)

Tactic:
rw [constantCoeff_map] at h

Premises used: MvPowerSeries.constantCoeff_map
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
⊢ IsUnit.{u_3} (M := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)

Tactic:
have : IsUnit (constantCoeff ψ.val) := isUnit_constantCoeff _ ψ.isUnit
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
this : IsUnit.{u_3} (M := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
⊢ IsUnit.{u_3} (M := S) ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)

Tactic:
rw [h] at this
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
this : IsUnit.{u_3} (M := S) ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
rcases : ∀ (c : Rˣ) (hc : (↑c : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ), IsUnit φ
⊢ IsUnit φ

Tactic:
rcases isUnit_of_map_unit f _ this with ⟨c, hc⟩

Premises used: isUnit_of_map_unit
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
this : IsUnit.{u_3} (M := S) ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
c : Rˣ
hc : (↑c : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ
⊢ IsUnit φ

Tactic:
.of_mul_eq_one (invOfUnit φ c) (mul_invOfUnit φ c hc.symm)

Premises used: IsUnit.of_mul_eq_one, MvPowerSeries.invOfUnit, MvPowerSeries.mul_invOfUnit, Eq.symm
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
R : Type u_2
S : Type u_3
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
φ : MvPowerSeries σ R
ψ : (MvPowerSeries σ S)ˣ
h :
  Eq.{u_3 + 1} (α := S) ((constantCoeff : (a : MvPowerSeries σ S) → S) (↑ψ : MvPowerSeries σ S) : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
this : IsUnit.{u_3} (M := S) ((f : (a : R) → S) ((constantCoeff : (a : MvPowerSeries σ R) → R) φ : R) : S)
c : Rˣ
hc : (↑c : R) = (constantCoeff : (a : MvPowerSeries σ R) → R) φ
⊢ IsUnit φ

Tactic:
exact .of_mul_eq_one (invOfUnit φ c) (mul_invOfUnit φ c hc.symm)
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
inst_1 : DecidableEq σ
n : σ →₀ ℕ
φ : MvPowerSeries σ k
⊢ Eq.{u_3 + 1} (α := k) ((coeff n : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (if n = 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)

Tactic:
coeff_inv_aux n _ φ

Premises used: MvPowerSeries.coeff_inv_aux, MvPowerSeries.inv, WellFounded.fixF, WellFounded.fix
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
rw :
  Eq.{u_3 + 1} (α := k) ((coeff 0 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
rw₁ :
  Eq.{u_3 + 1} (α := k)
    (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
              if x.2 < 0 then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := k) (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)

Tactic:
rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_inv, if_pos, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
rw :
  Eq.{u_3 + 1} (α := k) ((coeff 0 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
rw₁ :
  Eq.{u_3 + 1} (α := k)
    (if Eq.{u_1 + 1} (α := σ →₀ ℕ) 0 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ 0,
              if x.2 < 0 then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := k) (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)

Tactic:
classical
  rw [← coeff_zero_eq_constantCoeff_apply, coeff_inv, if_pos rfl]

Premises used: MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPowerSeries.coeff_inv, if_pos, rfl
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : φ⁻¹ = 0
⊢ Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)

Tactic:
simpa using congr_arg constantCoeff h

Premises used: MvPowerSeries.constantCoeff, congr_arg, DFunLike.coe
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
rw :
  Eq.{u_3 + 1} (α := k)
    (if n = 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
⊢ Eq.{u_3 + 1} (α := k) ((coeff n : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)

Tactic:
rw [coeff_inv]

Premises used: MvPowerSeries.coeff_inv
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
pos :
  n = 0 →
    Eq.{u_3 + 1} (α := k) (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
      ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
neg :
  ¬n = 0 →
    HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
        (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
            if x.2 < n then
              HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
            else 0 :
          k) =
      (coeff n : (a : MvPowerSeries σ k) → k) 0
⊢ Eq.{u_3 + 1} (α := k)
    (if n = 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
h_1 : n = 0
⊢ Eq.{u_3 + 1} (α := k) (((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)

Tactic:
simp only [h, map_zero, zero_mul, inv_zero, neg_zero]

Premises used: inv_zero, MulZeroClass.zero_mul, map_zero, neg_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
h_1 : ¬n = 0
⊢ HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
      (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
              ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
          else 0 :
        k) =
    (coeff n : (a : MvPowerSeries σ k) → k) 0

Tactic:
simp only [h, map_zero, zero_mul, inv_zero, neg_zero]

Premises used: inv_zero, MulZeroClass.zero_mul, map_zero, neg_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
n : σ →₀ ℕ
rw rw₁ rw₂ :
  Eq.{u_3 + 1} (α := k)
    (if n = 0 then ((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : MvPowerSeries σ k) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Finsupp.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : MvPowerSeries σ k) → k) φ : k)
                  ((coeff x.2 : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)
⊢ Eq.{u_3 + 1} (α := k) ((coeff n : (a : MvPowerSeries σ k) → k) φ⁻¹ : k)
    ((coeff n : (a : MvPowerSeries σ k) → k) 0 : k)

Tactic:
classical
      rw [coeff_inv]
      split_ifs <;>
        simp only [h, map_zero, zero_mul, inv_zero, neg_zero]

Premises used: inv_zero, MulZeroClass.zero_mul, MvPowerSeries.coeff_inv, map_zero, neg_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
rw : Eq.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) 0 : k) (0 : k)
rw₁ rw₂ : Eq.{u_3 + 1} (α := k) 0 0
⊢ Eq (α := MvPowerSeries σ k) 0⁻¹ 0

Tactic:
rw [inv_eq_zero, constantCoeff_zero]

Premises used: MvPowerSeries.constantCoeff_zero, MvPowerSeries.inv_eq_zero
-- Module: Mathlib.RingTheory.MvPowerSeries.Inverse
Goal:
σ : Type u_1
k : Type u_3
inst : Field k
φ : MvPowerSeries σ k
h : Ne.{u_3 + 1} (α := k) ((constantCoeff : (a : MvPowerSeries σ k) → k) φ : k) (0 : k)
⊢ φ.invOfUnit (Units.mk0 ((constantCoeff : (a : MvPowerSeries σ k) → k) φ) h) = φ⁻¹

Tactic:
rfl

Premises used: MvPowerSeries.invOfUnit, MvPowerSeries.inv, WellFounded.fixF, WellFounded.fix, rfl