awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
⊢ ∀ (a : (Unit →₀ ℕ) × (Unit →₀ ℕ)),
    Membership.mem (γ := Finset ((Unit →₀ ℕ) × (Unit →₀ ℕ))) (@antidiagonal _ Finsupp.instAddMonoid _ (single () n)) a →
      (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ))
          match (motive := (Unit →₀ ℕ) × (Unit →₀ ℕ) → ℕ × ℕ) a with
          | (f, g) => ((f : (a : Unit) → ℕ) (), (g : (a : Unit) → ℕ) ()) with
        | (a, b) => (single () a, single () b)) =
        a

Tactic:
aesop
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : n ≤ j
⊢ (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0

Tactic:
aesop
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
neg :
  HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
      ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R) =
    HMul.hMul (α := R) (β := R)
      ((MvPowerSeries.coeff
              (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                | (a, b) => (single () a, single () b)).1 :
            (a : MvPowerSeries Unit R) → R)
          φ :
        R)
      ((MvPowerSeries.coeff
              (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                | (a, b) => (single () a, single () b)).2 :
            (a : MvPowerSeries Unit R) → R)
          (MvPowerSeries.inv.aux a φ) :
        R)
neg₁ :
  LT.lt (α := Unit →₀ ℕ)
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
      | (a, b) => (single () a, single () b)).2
    (single () n)
⊢ (if (i, j).2 < n then
      HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
        ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R)
    else 0) =
    if
        LT.lt (α := Unit →₀ ℕ)
          (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2
          (single () n) then
      HMul.hMul (α := R) (β := R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).1 :
              (a : MvPowerSeries Unit R) → R)
            φ :
          R)
        ((MvPowerSeries.coeff
                (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                  | (a, b) => (single () a, single () b)).2 :
              (a : MvPowerSeries Unit R) → R)
            (MvPowerSeries.inv.aux a φ) :
          R)
    else 0

Tactic:
rw [if_pos H, if_pos]

Premises used: if_pos
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
⊢ HMul.hMul (α := R) (β := R) ((coeff (i, j).1 : (a : R⟦X⟧) → R) φ : R)
      ((coeff (i, j).2 : (a : R⟦X⟧) → R) (MvPowerSeries.inv.aux a φ) : R) =
    HMul.hMul (α := R) (β := R)
      ((MvPowerSeries.coeff
              (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                | (a, b) => (single () a, single () b)).1 :
            (a : MvPowerSeries Unit R) → R)
          φ :
        R)
      ((MvPowerSeries.coeff
              (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
                | (a, b) => (single () a, single () b)).2 :
            (a : MvPowerSeries Unit R) → R)
          (MvPowerSeries.inv.aux a φ) :
        R)

Tactic:
rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
⊢ LT.lt (α := Unit →₀ ℕ)
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
      | (a, b) => (single () a, single () b)).2
    (single () n)

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

Premises used: And.intro, LT.lt.not_ge
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
neg :
  LE.le (α := Unit →₀ ℕ)
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
      | (a, b) => (single () a, single () b)).2
    (single () n)
neg₁ :
  ∀
    (hh :
      LE.le (α := Unit →₀ ℕ) (single () n)
        (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
          | (a, b) => (single () a, single () b)).2),
    n ≤ j
⊢ LT.lt (α := Unit →₀ ℕ)
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
      | (a, b) => (single () a, single () b)).2
    (single () n)

Tactic:
refine ⟨?_, fun hh ↦ H.not_ge ?_⟩
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
⊢ LE.le (α := ℕ)
    (((match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
            | (a, b) => (single () a, single () b)).2 :
          (a : Unit) → ℕ)
        PUnit.unit :
      ℕ)
    ((single () n : (a : Unit) → ℕ) PUnit.unit : ℕ)

Tactic:
simpa [Finsupp.single_eq_same] using le_of_lt H

Premises used: Finsupp.single_eq_same, le_of_lt
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
a : R
φ : R⟦X⟧
h : ¬n = 0
i j : ℕ
_hij : (i, j) ∈ @antidiagonal _ Nat.instAddMonoid _ n
H : j < n
hh :
  LE.le (α := Unit →₀ ℕ) (single () n)
    (match (motive := ℕ × ℕ → (Unit →₀ ℕ) × (Unit →₀ ℕ)) (i, j) with
      | (a, b) => (single () a, single () b)).2
⊢ n ≤ j

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

Premises used: Unit.unit, Finsupp.single_eq_same
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
n : ℕ
φ : R⟦X⟧
u : Rˣ
⊢ (coeff n : (a : R⟦X⟧) → R) (φ.invOfUnit u) =
    if n = 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
          if x.2 < n then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (φ.invOfUnit u) : R)
          else 0

Tactic:
coeff_inv_aux n (↑u⁻¹ : R) φ

Premises used: Units.val, PowerSeries.coeff_inv_aux, PowerSeries.invOfUnit, MvPowerSeries.invOfUnit, Inv.inv
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
u : Rˣ
rw : (coeff 0 : (a : R⟦X⟧) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)
rw₁ :
  (if Eq (α := ℕ) 0 0 then (↑u⁻¹ : R)
    else
      -(↑u⁻¹ : R) *
        ∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ 0,
          if x.2 < 0 then
            HMul.hMul (α := R) (β := R) ((coeff x.1 : (a : R⟦X⟧) → R) φ : R)
              ((coeff x.2 : (a : R⟦X⟧) → R) (φ.invOfUnit u) : R)
          else 0) =
    (↑u⁻¹ : R)
rw₂ rw₃ : (↑u⁻¹ : R) = (↑u⁻¹ : R)
⊢ (constantCoeff : (a : R⟦X⟧) → R) (φ.invOfUnit u) = (↑u⁻¹ : R)

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

Premises used: PowerSeries.coeff_invOfUnit, if_pos, PowerSeries.coeff_zero_eq_constantCoeff_apply, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
u : Rˣ
h : (constantCoeff : (a : R⟦X⟧) → R) φ = (↑u : R)
⊢ φ * φ.invOfUnit u = 1

Tactic:
MvPowerSeries.mul_invOfUnit φ u <| h

Premises used: PowerSeries.invOfUnit, MvPowerSeries.mul_invOfUnit
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
u : Rˣ
h : (constantCoeff : (a : R⟦X⟧) → R) φ = (↑u : R)
⊢ φ.invOfUnit u * φ = 1

Tactic:
MvPowerSeries.invOfUnit_mul φ u h

Premises used: PowerSeries.invOfUnit, MvPowerSeries.invOfUnit_mul
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
⊢ IsUnit φ ↔ IsUnit (M := R) ((constantCoeff : (a : R⟦X⟧) → R) φ : R)

Tactic:
MvPowerSeries.isUnit_iff_constantCoeff

Premises used: MvPowerSeries.isUnit_iff_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
⊢ HSub.hSub (β := R⟦X⟧) φ ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧) =
    HMul.hMul (α := R⟦X⟧) (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ) X

Tactic:
sub_eq_iff_eq_add.mpr (eq_shift_mul_X_add_const φ)

Premises used: Iff.mpr, sub_eq_iff_eq_add, PowerSeries.eq_shift_mul_X_add_const
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
inst : Ring R
φ : R⟦X⟧
⊢ HSub.hSub (β := R⟦X⟧) φ ((C : (a : R) → R⟦X⟧) ((constantCoeff : (a : R⟦X⟧) → R) φ : R) : R⟦X⟧) =
    HMul.hMul (α := R⟦X⟧) X (mk fun (p : ℕ) ↦ (coeff (p + 1) : (a : R⟦X⟧) → R) φ)

Tactic:
sub_eq_iff_eq_add.mpr (eq_X_mul_shift_add_const φ)

Premises used: Iff.mpr, PowerSeries.eq_X_mul_shift_add_const, sub_eq_iff_eq_add
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ : k⟦X⟧
⊢ φ⁻¹ = inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ

Tactic:
rfl

Premises used: PowerSeries.inv.aux, MvPowerSeries.inv, WellFounded.fixF, WellFounded.fix, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
n : ℕ
φ : k⟦X⟧
rw :
  Eq (α := k) ((coeff n : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
    (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k)
                  ((coeff x.2 : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
              else 0 :
            k) :
      k)
rw₁ rw₂ :
  Eq (α := k)
    (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k)
                  ((coeff x.2 : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
              else 0 :
            k) :
      k)
    (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k)
                  ((coeff x.2 : (a : k⟦X⟧) → k) (inv.aux ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ φ : k⟦X⟧) : k)
              else 0 :
            k) :
      k)
⊢ Eq (α := k) ((coeff n : (a : k⟦X⟧) → k) φ⁻¹ : k)
    (if n = 0 then ((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹
      else
        HMul.hMul (α := k) (β := k) (-((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)
          (∑ x ∈ @antidiagonal _ Nat.instAddMonoid _ n,
              if x.2 < n then
                HMul.hMul (α := k) (β := k) ((coeff x.1 : (a : k⟦X⟧) → k) φ : k) ((coeff x.2 : (a : k⟦X⟧) → k) φ⁻¹ : k)
              else 0 :
            k) :
      k)

Tactic:
rw [inv_eq_inv_aux, coeff_inv_aux n (constantCoeff φ)⁻¹ φ]

Premises used: PowerSeries.coeff_inv_aux, PowerSeries.constantCoeff, Inv.inv, PowerSeries.inv_eq_inv_aux, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ : k⟦X⟧
⊢ Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) φ⁻¹ : k) (((constantCoeff : (a : k⟦X⟧) → k) φ)⁻¹ : k)

Tactic:
MvPowerSeries.constantCoeff_inv φ

Premises used: MvPowerSeries.constantCoeff_inv
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ : k⟦X⟧
⊢ φ⁻¹ = 0 ↔ Eq (α := k) ((constantCoeff : (a : k⟦X⟧) → k) φ : k) (0 : k)

Tactic:
MvPowerSeries.inv_eq_zero

Premises used: MvPowerSeries.inv_eq_zero
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
⊢ Eq.{u_2 + 1} (α := k⟦X⟧) 0⁻¹ 0

Tactic:
MvPowerSeries.zero_inv

Premises used: MvPowerSeries.zero_inv
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ : k⟦X⟧
h : Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) φ : k) (0 : k)
⊢ φ.invOfUnit (Units.mk0 ((constantCoeff : (a : k⟦X⟧) → k) φ) h) = φ⁻¹

Tactic:
rfl

Premises used: PowerSeries.invOfUnit, MvPowerSeries.invOfUnit, MvPowerSeries.inv, WellFounded.fixF, WellFounded.fix, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ : k⟦X⟧
u : kˣ
h : (constantCoeff : (a : k⟦X⟧) → k) φ = (↑u : k)
⊢ φ.invOfUnit u = φ⁻¹

Tactic:
MvPowerSeries.invOfUnit_eq' φ _ h

Premises used: PowerSeries.invOfUnit, MvPowerSeries.invOfUnit_eq'
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ : k⟦X⟧
h : Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) φ : k) (0 : k)
⊢ φ * φ⁻¹ = 1

Tactic:
MvPowerSeries.mul_inv_cancel φ h

Premises used: MvPowerSeries.mul_inv_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ : k⟦X⟧
h : Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) φ : k) (0 : k)
⊢ φ⁻¹ * φ = 1

Tactic:
MvPowerSeries.inv_mul_cancel φ h

Premises used: MvPowerSeries.inv_mul_cancel
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ₁ φ₂ φ₃ : k⟦X⟧
h : Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) φ₃ : k) (0 : k)
⊢ φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂

Tactic:
MvPowerSeries.eq_mul_inv_iff_mul_eq h

Premises used: MvPowerSeries.eq_mul_inv_iff_mul_eq
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ ψ : k⟦X⟧
h : Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) ψ : k) (0 : k)
⊢ φ = ψ⁻¹ ↔ φ * ψ = 1

Tactic:
MvPowerSeries.eq_inv_iff_mul_eq_one h

Premises used: MvPowerSeries.eq_inv_iff_mul_eq_one
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ ψ : k⟦X⟧
h : Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) ψ : k) (0 : k)
⊢ ψ⁻¹ = φ ↔ φ * ψ = 1

Tactic:
MvPowerSeries.inv_eq_iff_mul_eq_one h

Premises used: MvPowerSeries.inv_eq_iff_mul_eq_one
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
φ ψ : k⟦X⟧
⊢ (φ * ψ)⁻¹ = ψ⁻¹ * φ⁻¹

Tactic:
MvPowerSeries.mul_inv_rev _ _

Premises used: MvPowerSeries.mul_inv_rev
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
r : k
⊢ Eq (α := k⟦X⟧) (((C : (a : k) → k⟦X⟧) r)⁻¹ : k⟦X⟧) ((C : (a : k) → k⟦X⟧) r⁻¹ : k⟦X⟧)

Tactic:
MvPowerSeries.C_inv _

Premises used: MvPowerSeries.C_inv
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
⊢ Eq.{u_2 + 1} (α := k⟦X⟧) X⁻¹ 0

Tactic:
MvPowerSeries.X_inv _

Premises used: PowerSeries.X, MvPowerSeries.X_inv
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
r : k
φ : k⟦X⟧
⊢ (r • φ)⁻¹ = r⁻¹ • φ⁻¹

Tactic:
MvPowerSeries.smul_inv _ _

Premises used: MvPowerSeries.smul_inv
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f.divXPowOrder : k) (0 : k)
⊢ Invertible (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f.divXPowOrder : k)

Tactic:
apply invertibleOfNonzero

Premises used: invertibleOfNonzero
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ Ne (α := k) ((constantCoeff : (a : k⟦X⟧) → k) f.divXPowOrder : k) (0 : k)

Tactic:
simpa [constantCoeff_divXPowOrder_eq_zero_iff.not]

Premises used: Iff.not, PowerSeries.constantCoeff_divXPowOrder_eq_zero_iff
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ f.divXPowOrder * Inv_divided_by_X_pow_order hf = 1

Tactic:
mul_invOfUnit (divXPowOrder f) (firstUnitCoeff hf) rfl

Premises used: PowerSeries.divXPowOrder, PowerSeries.mul_invOfUnit, PowerSeries.firstUnitCoeff, PowerSeries.Inv_divided_by_X_pow_order, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
rw : f.divXPowOrder * Inv_divided_by_X_pow_order hf = 1
⊢ Inv_divided_by_X_pow_order hf * f.divXPowOrder = 1

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ f.divXPowOrder * Inv_divided_by_X_pow_order hf = 1

Tactic:
exact mul_invOfUnit (divXPowOrder f) (firstUnitCoeff hf) rfl

Premises used: PowerSeries.divXPowOrder, PowerSeries.mul_invOfUnit, PowerSeries.firstUnitCoeff, rfl
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ (↑f.Unit_of_divided_by_X_pow_order : k⟦X⟧) = f.divXPowOrder

Tactic:
simp only [Unit_of_divided_by_X_pow_order, dif_neg hf, Units.val_mk]

Premises used: dif_neg, Units.val_mk, PowerSeries.Unit_of_divided_by_X_pow_order
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
⊢ Eq.{u_2 + 1} (α := k⟦X⟧ˣ) (Unit_of_divided_by_X_pow_order 0) 1

Tactic:
simp only [Unit_of_divided_by_X_pow_order, dif_pos]

Premises used: dif_pos, PowerSeries.Unit_of_divided_by_X_pow_order
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = f.divXPowOrder
rw : IsUnit f.divXPowOrder
⊢ IsUnit f

Tactic:
rw [h]
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = f.divXPowOrder
⊢ IsUnit f.divXPowOrder

Tactic:
isUnit_divided_by_X_pow_order hf

Premises used: PowerSeries.isUnit_divided_by_X_pow_order
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : f = f.divXPowOrder
⊢ IsUnit f.divXPowOrder

Tactic:
exact isUnit_divided_by_X_pow_order hf

Premises used: PowerSeries.isUnit_divided_by_X_pow_order
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
⊢ f.order = 0

Tactic:
simp [order_zero_of_unit h]

Premises used: PowerSeries.order_zero_of_unit
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
⊢ f.order = 0

Tactic:
have : f.order = 0 := by
      simp [order_zero_of_unit h]
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
rw : f.divXPowOrder
| f

Tactic:
rw [← X_pow_order_mul_divXPowOrder (f := f), this, ENat.toNat_zero,
      pow_zero, one_mul]

Premises used: ENat.toNat_zero, pow_zero, PowerSeries.X_pow_order_mul_divXPowOrder, one_mul
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : IsUnit f
this : f.order = 0
conv_lhs : f = f.divXPowOrder
conv_lhs₁ : f.divXPowOrder = f.divXPowOrder
⊢ f = f.divXPowOrder

Tactic:
conv_lhs => rw [← X_pow_order_mul_divXPowOrder (f := f), this, ENat.toNat_zero,
      pow_zero, one_mul]

Premises used: ENat.toNat_zero, pow_zero, PowerSeries.X_pow_order_mul_divXPowOrder, one_mul
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
f : R →+* S
inst_2 : IsLocalHom (R := R) (S := S) f
⊢ IsLocalHom (R := R⟦X⟧) (S := S⟦X⟧) (map f)

Tactic:
MvPowerSeries.map.isLocalHom f

Premises used: PowerSeries.map, MvPowerSeries.map.isLocalHom
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : Associated (HPow.hPow (α := k⟦X⟧) X f.order.toNat) f
⊢ ∃ (n : ℕ), Associated (HPow.hPow (α := k⟦X⟧) X n) f

Tactic:
use f.order.toNat

Premises used: PowerSeries.order, ENat.toNat
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : HPow.hPow (α := k⟦X⟧) X f.order.toNat * (↑f.Unit_of_divided_by_X_pow_order : k⟦X⟧) = f
⊢ Associated (HPow.hPow (α := k⟦X⟧) X f.order.toNat) f

Tactic:
use Unit_of_divided_by_X_pow_order f

Premises used: PowerSeries.Unit_of_divided_by_X_pow_order
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
h : HPow.hPow (α := k⟦X⟧) X f.order.toNat * f.divXPowOrder = f
⊢ HPow.hPow (α := k⟦X⟧) X f.order.toNat * (↑f.Unit_of_divided_by_X_pow_order : k⟦X⟧) = f

Tactic:
simp only [Unit_of_divided_by_X_pow_order_nonzero hf]

Premises used: PowerSeries.Unit_of_divided_by_X_pow_order_nonzero
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ HPow.hPow (α := k⟦X⟧) X f.order.toNat * f.divXPowOrder = f

Tactic:
X_pow_order_mul_divXPowOrder

Premises used: PowerSeries.X_pow_order_mul_divXPowOrder
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
f : k⟦X⟧
hf : f ≠ 0
⊢ HPow.hPow (α := k⟦X⟧) X f.order.toNat * f.divXPowOrder = f

Tactic:
exact X_pow_order_mul_divXPowOrder

Premises used: PowerSeries.X_pow_order_mul_divXPowOrder
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
⊢ UniqueFactorizationMonoid.{u_2} k⟦X⟧

Tactic:
hasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid

Premises used: PowerSeries.hasUnitMulPowIrreducibleFactorization, IsDiscreteValuationRing.HasUnitMulPowIrreducibleFactorization.toUniqueFactorizationMonoid
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
⊢ IsDiscreteValuationRing.{u_2} k⟦X⟧

Tactic:
ofHasUnitMulPowIrreducibleFactorization hasUnitMulPowIrreducibleFactorization

Premises used: IsDiscreteValuationRing.ofHasUnitMulPowIrreducibleFactorization, PowerSeries.hasUnitMulPowIrreducibleFactorization
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
R : Type u_1
k : Type u_2
inst : Field k
⊢ IsNoetherianRing.{u_2} k⟦X⟧

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
rw : 1 ∉ Ideal.span {X} ∧ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J
⊢ Ideal.IsMaximal (α := k⟦X⟧) (Ideal.span {X})

Tactic:
rw [Ideal.isMaximal_iff]

Premises used: Ideal.isMaximal_iff
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
left : 1 ∉ Ideal.span {X}
right : ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J
⊢ 1 ∉ Ideal.span {X} ∧ ∀ (J : Ideal k⟦X⟧) (x : k⟦X⟧), Ideal.span {X} ≤ J → x ∉ Ideal.span {X} → x ∈ J → 1 ∈ J

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
left : ¬Dvd.dvd.{u_2} (α := k⟦X⟧) X 1
⊢ 1 ∉ Ideal.span {X}

Tactic:
rw [Ideal.mem_span_singleton]

Premises used: Ideal.mem_span_singleton
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
⊢ ¬Dvd.dvd.{u_2} (α := k⟦X⟧) X 1

Tactic:
Prime.not_dvd_one X_prime

Premises used: PowerSeries.X_prime, Prime.not_dvd_one
-- Module: Mathlib.RingTheory.PowerSeries.Inverse
Goal:
k : Type u_2
inst : Field k
⊢ ¬Dvd.dvd.{u_2} (α := k⟦X⟧) X 1

Tactic:
exact Prime.not_dvd_one X_prime

Premises used: PowerSeries.X_prime, Prime.not_dvd_one