awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
rw :
  ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    HMul.hMul (β := R⟦ℤ⟧)
      (HMul.hMul (α := R⟦ℤ⟧) ((single (-order x) : (a : R) → R⟦ℤ⟧) 1) ((single (order x) : (a : R) → R⟦ℤ⟧) 1))
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
rw₁ :
  ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((single (-order x + order x) : (a : R) → R⟦ℤ⟧) (HMul.hMul (α := R) 1 1) : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
rw₂ :
  ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((single 0 : (a : R) → R⟦ℤ⟧) (HMul.hMul (α := R) 1 1) : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
rw₃ :
  ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((single 0 : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
rw₄ :
  ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((HahnSeries.C : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
rw₅ :
  ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) (1 : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
rw₆ rw₇ :
  Eq (α := R⟦ℤ⟧) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
    (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)
⊢ ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    (single (-order x) : (a : R) → R⟦ℤ⟧) 1 *
      HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) ((single (order x) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
        (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart : R⟦ℤ⟧)

Tactic:
rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]

Premises used: HahnSeries.single_mul_single, mul_assoc, neg_add_cancel, HahnSeries.C_one, mul_one, HahnSeries.C_apply, one_mul
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
n : ℕ
f : R⸨X⸩
hn : (↑n : ℤ) = order f
⊢ ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧)
      (HPow.hPow (α := R⟦X⟧) PowerSeries.X n * f.powerSeriesPart) =
    f

Tactic:
simp only [map_mul, map_pow, ofPowerSeries_X, single_pow, nsmul_eq_mul, mul_one, one_pow, hn,
    single_order_mul_powerSeriesPart]

Premises used: one_pow, HahnSeries.single_pow, LaurentSeries.single_order_mul_powerSeriesPart, map_pow, HahnSeries.ofPowerSeries_X, map_mul, nsmul_eq_mul, mul_one
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommSemiring R
⊢ Eq (α := (a : R⟦X⟧) → R⸨X⸩) (⇑(algebraMap R⟦X⟧ R⸨X⸩) : (a : R⟦X⟧) → R⸨X⸩)
    (⇑(ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ IsUnit (M := R⸨X⸩)
    ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
        (↑(Subtype.mk (p := fun (x : R⟦X⟧) ↦ Membership.mem (γ := Submonoid R⟦X⟧) (Submonoid.powers PowerSeries.X) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := R⟦X⟧) PowerSeries.X x) n) ⋯) :
          R⟦X⟧) :
      R⸨X⸩)

Tactic:
⟨⟨single (n : ℤ) 1, single (-n : ℤ) 1, ?_, ?_⟩, ?_⟩

Premises used: HahnSeries.single, IsUnit, Nat.cast, Units.mk, Exists.intro, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
refine_1 : HMul.hMul (α := R⸨X⸩) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1) ((single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1) = 1
refine_2 : HMul.hMul (α := R⸨X⸩) ((single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1) = 1
refine_3 :
  Eq (α := R⸨X⸩)
    ((↑{ val := (single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1, inv := (single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1, val_inv := ⋯,
            inv_val := ⋯ } :
        R⸨X⸩) :
      R⸨X⸩)
    ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
        (↑(Subtype.mk (p := fun (x : R⟦X⟧) ↦ Membership.mem (γ := Submonoid R⟦X⟧) (Submonoid.powers PowerSeries.X) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := R⟦X⟧) PowerSeries.X x) n) ⋯) :
          R⟦X⟧) :
      R⸨X⸩)
⊢ IsUnit (M := R⸨X⸩)
    ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
        (↑(Subtype.mk (p := fun (x : R⟦X⟧) ↦ Membership.mem (γ := Submonoid R⟦X⟧) (Submonoid.powers PowerSeries.X) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := R⟦X⟧) PowerSeries.X x) n) ⋯) :
          R⟦X⟧) :
      R⸨X⸩)

Tactic:
refine ⟨⟨single (n : ℤ) 1, single (-n : ℤ) 1, ?_, ?_⟩, ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ HMul.hMul (α := R⸨X⸩) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1) ((single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ HMul.hMul (α := R⸨X⸩) ((single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1) = 1

Tactic:
simp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
refine_3 :
  Eq (α := R⸨X⸩) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
    (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) (HPow.hPow (α := R⟦X⟧) PowerSeries.X n) : R⟦ℤ⟧)
⊢ Eq (α := R⸨X⸩)
    ((↑{ val := (single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1, inv := (single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1, val_inv := ⋯,
            inv_val := ⋯ } :
        R⸨X⸩) :
      R⸨X⸩)
    ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
        (↑(Subtype.mk (p := fun (x : R⟦X⟧) ↦ Membership.mem (γ := Submonoid R⟦X⟧) (Submonoid.powers PowerSeries.X) x)
              ((fun (x : ℕ) ↦ HPow.hPow (α := R⟦X⟧) PowerSeries.X x) n) ⋯) :
          R⟦X⟧) :
      R⸨X⸩)

Tactic:
dsimp
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
refine_3 refine_3₁ :
  Eq.{u_1 + 1} (α := R⸨X⸩) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1)
⊢ Eq (α := R⸨X⸩) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
    (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) (HPow.hPow (α := R⟦X⟧) PowerSeries.X n) : R⟦ℤ⟧)

Tactic:
rw [ofPowerSeries_X_pow]

Premises used: HahnSeries.ofPowerSeries_X_pow
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
pos :
  ∀ (h : 0 ≤ order z),
    ∃ (x : R⟦X⟧ × ↥(Submonoid.powers PowerSeries.X)),
      HMul.hMul (β := R⸨X⸩) z ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) (↑x.2 : R⟦X⟧) : R⸨X⸩) =
        (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) x.1
neg :
  ∀ (h : order z < 0),
    ∃ (x : R⟦X⟧ × ↥(Submonoid.powers PowerSeries.X)),
      HMul.hMul (β := R⸨X⸩) z ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) (↑x.2 : R⟦X⟧) : R⸨X⸩) =
        (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) x.1
⊢ ∃ (x : R⟦X⟧ × ↥(Submonoid.powers PowerSeries.X)),
    HMul.hMul (β := R⸨X⸩) z ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) (↑x.2 : R⟦X⟧) : R⸨X⸩) =
      (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) x.1

Tactic:
by_cases! h : 0 ≤ z.order

Premises used: HahnSeries.order
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : 0 ≤ order z
⊢ ∃ (x : R⟦X⟧ × ↥(Submonoid.powers PowerSeries.X)),
    HMul.hMul (β := R⸨X⸩) z ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) (↑x.2 : R⟦X⟧) : R⸨X⸩) =
      (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) x.1

Tactic:
⟨⟨PowerSeries.X ^ Int.natAbs z.order * powerSeriesPart z, 1⟩, ?_⟩

Premises used: HahnSeries.order, HMul.hMul, Prod.mk, PowerSeries.X, HPow.hPow, LaurentSeries.powerSeriesPart, Int.natAbs, Exists.intro, OfNat.ofNat
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : 0 ≤ order z
pos :
  z *
      (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
        (↑(HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs * z.powerSeriesPart, 1).2 : R⟦X⟧) =
    (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
      (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs * z.powerSeriesPart, 1).1
⊢ ∃ (x : R⟦X⟧ × ↥(Submonoid.powers PowerSeries.X)),
    HMul.hMul (β := R⸨X⸩) z ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) (↑x.2 : R⟦X⟧) : R⸨X⸩) =
      (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) x.1

Tactic:
refine ⟨⟨PowerSeries.X ^ Int.natAbs z.order * powerSeriesPart z, 1⟩, ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : 0 ≤ order z
pos :
  z =
    HMul.hMul (α := R⸨X⸩) (β := R⸨X⸩) ((single (↑(order z).natAbs : ℤ) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) z.powerSeriesPart : R⟦ℤ⟧)
⊢ z *
      (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
        (↑(HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs * z.powerSeriesPart, 1).2 : R⟦X⟧) =
    (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
      (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs * z.powerSeriesPart, 1).1

Tactic:
simp only [map_one, mul_one, map_mul, coe_algebraMap, ofPowerSeries_X_pow,
        Submonoid.coe_one]

Premises used: HahnSeries.ofPowerSeries_X_pow, LaurentSeries.coe_algebraMap, Submonoid.coe_one, map_mul, map_one, mul_one
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : 0 ≤ order z
pos :
  z =
    HMul.hMul (α := R⸨X⸩) (β := R⸨X⸩) ((single (order z) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) z.powerSeriesPart : R⟦ℤ⟧)
pos₁ pos₂ : z = z
⊢ z =
    HMul.hMul (α := R⸨X⸩) (β := R⸨X⸩) ((single (↑(order z).natAbs : ℤ) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) z.powerSeriesPart : R⟦ℤ⟧)

Tactic:
rw [Int.natAbs_of_nonneg h, single_order_mul_powerSeriesPart]

Premises used: LaurentSeries.single_order_mul_powerSeriesPart, Int.natAbs_of_nonneg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ ∃ (x : R⟦X⟧ × ↥(Submonoid.powers PowerSeries.X)),
    HMul.hMul (β := R⸨X⸩) z ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) (↑x.2 : R⟦X⟧) : R⸨X⸩) =
      (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) x.1

Tactic:
⟨⟨powerSeriesPart z, PowerSeries.X ^ Int.natAbs z.order, ⟨_, rfl⟩⟩, ?_⟩

Premises used: HahnSeries.order, Prod.mk, PowerSeries.X, Subtype.mk, HPow.hPow, LaurentSeries.powerSeriesPart, Int.natAbs, Exists.intro, rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
neg :
  HMul.hMul (β := R⸨X⸩) z
      ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
          (↑(z.powerSeriesPart,
                  Subtype.mk (p := fun (x : R⟦X⟧) ↦
                    Membership.mem (γ := Submonoid R⟦X⟧) (Submonoid.powers PowerSeries.X) x)
                    (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) ⋯).2 :
            R⟦X⟧) :
        R⸨X⸩) =
    (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
      (z.powerSeriesPart,
          Subtype.mk (p := fun (x : R⟦X⟧) ↦ Membership.mem (γ := Submonoid R⟦X⟧) (Submonoid.powers PowerSeries.X) x)
            (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) ⋯).1
⊢ ∃ (x : R⟦X⟧ × ↥(Submonoid.powers PowerSeries.X)),
    HMul.hMul (β := R⸨X⸩) z ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) (↑x.2 : R⟦X⟧) : R⸨X⸩) =
      (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) x.1

Tactic:
refine ⟨⟨powerSeriesPart z, PowerSeries.X ^ Int.natAbs z.order, ⟨_, rfl⟩⟩, ?_⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
neg :
  HMul.hMul (β := R⸨X⸩) z
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧)
          (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) :
        R⟦ℤ⟧) =
    (single (-order z) : (a : R) → R⟦ℤ⟧) 1 * z
⊢ HMul.hMul (β := R⸨X⸩) z
      ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
          (↑(z.powerSeriesPart,
                  Subtype.mk (p := fun (x : R⟦X⟧) ↦
                    Membership.mem (γ := Submonoid R⟦X⟧) (Submonoid.powers PowerSeries.X) x)
                    (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) ⋯).2 :
            R⟦X⟧) :
        R⸨X⸩) =
    (algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩)
      (z.powerSeriesPart,
          Subtype.mk (p := fun (x : R⟦X⟧) ↦ Membership.mem (γ := Submonoid R⟦X⟧) (Submonoid.powers PowerSeries.X) x)
            (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) ⋯).1

Tactic:
simp only [coe_algebraMap, ofPowerSeries_powerSeriesPart]

Premises used: LaurentSeries.ofPowerSeries_powerSeriesPart, LaurentSeries.coe_algebraMap
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
neg :
  HMul.hMul (β := R⸨X⸩) z
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧)
          (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) :
        R⟦ℤ⟧) =
    z * (single (-order z) : (a : R) → R⟦ℤ⟧) 1
⊢ HMul.hMul (β := R⸨X⸩) z
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧)
          (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) :
        R⟦ℤ⟧) =
    (single (-order z) : (a : R) → R⟦ℤ⟧) 1 * z

Tactic:
rw [mul_comm _ z]

Premises used: mul_comm
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ HMul.hMul (β := R⸨X⸩) z
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧)
          (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) :
        R⟦ℤ⟧) =
    z * (single (-order z) : (a : R) → R⟦ℤ⟧) 1

Tactic:
congr rfl ?_

Premises used: congr, rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
neg :
  Eq (α := R⟦ℤ⟧)
    (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) :
      R⟦ℤ⟧)
    ((single (-order z) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)
⊢ HMul.hMul (β := R⸨X⸩) z
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧)
          (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) :
        R⟦ℤ⟧) =
    z * (single (-order z) : (a : R) → R⟦ℤ⟧) 1

Tactic:
refine congr rfl ?_

Premises used: congr, rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
neg : order z ≤ 0
⊢ Eq (α := R⟦ℤ⟧)
    (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) (HPow.hPow (α := R⟦X⟧) PowerSeries.X (order z).natAbs) :
      R⟦ℤ⟧)
    ((single (-order z) : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)

Tactic:
rw [ofPowerSeries_X_pow, Int.ofNat_natAbs_of_nonpos]

Premises used: HahnSeries.ofPowerSeries_X_pow, Int.ofNat_natAbs_of_nonpos
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ order z ≤ 0

Tactic:
h.le

Premises used: LT.lt.le
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : order z < 0
⊢ order z ≤ 0

Tactic:
exact h.le

Premises used: LT.lt.le
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
x y : R⟦X⟧
rw : x = y → ∃ (c : ↥(Submonoid.powers PowerSeries.X)), (↑c : R⟦X⟧) * x = (↑c : R⟦X⟧) * y
⊢ Eq (α := R⸨X⸩) ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) x : R⸨X⸩)
      ((algebraMap R⟦X⟧ R⸨X⸩ : (a : R⟦X⟧) → R⸨X⸩) y : R⸨X⸩) →
    ∃ (c : ↥(Submonoid.powers PowerSeries.X)), (↑c : R⟦X⟧) * x = (↑c : R⟦X⟧) * y

Tactic:
rw [coe_algebraMap, ofPowerSeries_injective.eq_iff]

Premises used: LaurentSeries.coe_algebraMap, Function.Injective.eq_iff, HahnSeries.ofPowerSeries_injective
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
x : R⟦X⟧
⊢ ∃ (c : ↥(Submonoid.powers PowerSeries.X)), (↑c : R⟦X⟧) * x = (↑c : R⟦X⟧) * x

Tactic:
⟨1, rfl⟩

Premises used: Exists.intro, OfNat.ofNat, rfl
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : CommRing R
x : R⟦X⟧
⊢ ∃ (c : ↥(Submonoid.powers PowerSeries.X)), (↑c : R⟦X⟧) * x = (↑c : R⟦X⟧) * x

Tactic:
exact ⟨1, rfl⟩
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
K : Type u_2
inst : Field K
⊢ IsFractionRing.{u_2, u_2} K⟦X⟧ K⸨X⸩

Tactic:
IsLocalization.of_le (Submonoid.powers (PowerSeries.X : K⟦X⟧)) _
    (powers_le_nonZeroDivisors_of_noZeroDivisors PowerSeries.X_ne_zero) fun _ hf =>
    isUnit_of_mem_nonZeroDivisors <| map_mem_nonZeroDivisors _ HahnSeries.ofPowerSeries_injective hf

Premises used: isUnit_of_mem_nonZeroDivisors, map_mem_nonZeroDivisors, Int, PowerSeries.X, powers_le_nonZeroDivisors_of_noZeroDivisors, Submonoid.powers, PowerSeries.X_ne_zero, IsLocalization.of_le, HahnSeries.ofPowerSeries_injective, HahnSeries.ofPowerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := R⟦ℤ⟧) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) 0) 0

Tactic:
(ofPowerSeries ℤ R).map_zero

Premises used: Int, RingHom.map_zero, HahnSeries.ofPowerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := R⟦ℤ⟧) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) 1) 1

Tactic:
(ofPowerSeries ℤ R).map_one

Premises used: RingHom.map_one, Int, HahnSeries.ofPowerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
f g : R⟦X⟧
⊢ ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) (f + g) =
    HAdd.hAdd (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) g : R⟦ℤ⟧)

Tactic:
(ofPowerSeries ℤ R).map_add _ _

Premises used: Int, RingHom.map_add, HahnSeries.ofPowerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R' : Type u_2
inst : Ring R'
f' g' : R'⟦X⟧
⊢ ((ofPowerSeries ℤ R' : R'⟦X⟧ →+* R'⟦ℤ⟧) : (a : R'⟦X⟧) → R'⟦ℤ⟧) (f' - g') =
    HSub.hSub (α := R'⟦ℤ⟧) (β := R'⟦ℤ⟧) (((ofPowerSeries ℤ R' : R'⟦X⟧ →+* R'⟦ℤ⟧) : (a : R'⟦X⟧) → R'⟦ℤ⟧) f' : R'⟦ℤ⟧)
      (((ofPowerSeries ℤ R' : R'⟦X⟧ →+* R'⟦ℤ⟧) : (a : R'⟦X⟧) → R'⟦ℤ⟧) g' : R'⟦ℤ⟧)

Tactic:
(ofPowerSeries ℤ R').map_sub _ _

Premises used: Int, RingHom.map_sub, HahnSeries.ofPowerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R' : Type u_2
inst : Ring R'
f' : R'⟦X⟧
⊢ Eq (α := R'⟦ℤ⟧) (((ofPowerSeries ℤ R' : R'⟦X⟧ →+* R'⟦ℤ⟧) : (a : R'⟦X⟧) → R'⟦ℤ⟧) (-f') : R'⟦ℤ⟧)
    (-((ofPowerSeries ℤ R' : R'⟦X⟧ →+* R'⟦ℤ⟧) : (a : R'⟦X⟧) → R'⟦ℤ⟧) f' : R'⟦ℤ⟧)

Tactic:
(ofPowerSeries ℤ R').map_neg _

Premises used: RingHom.map_neg, Int, HahnSeries.ofPowerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
f g : R⟦X⟧
⊢ ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) (f * g) =
    HMul.hMul (α := R⟦ℤ⟧) (β := R⟦ℤ⟧) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f : R⟦ℤ⟧)
      (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) g : R⟦ℤ⟧)

Tactic:
(ofPowerSeries ℤ R).map_mul _ _

Premises used: Int, RingHom.map_mul, HahnSeries.ofPowerSeries
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
i : ℤ
ofNat :
  ∀ (a : ℕ),
    Eq (α := R) (HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f) (Int.ofNat a) : R)
      (if Int.ofNat a < 0 then 0 else (coeff (Int.ofNat a).natAbs : (a : R⟦X⟧) → R) f : R)
negSucc :
  ∀ (a : ℕ),
    Eq (α := R) (HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f) (Int.negSucc a) : R)
      (if Int.negSucc a < 0 then 0 else (coeff (Int.negSucc a).natAbs : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) (HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f) i : R)
    (if i < 0 then 0 else (coeff i.natAbs : (a : R⟦X⟧) → R) f : R)

Tactic:
cases i
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
a : ℕ
ofNat :
  Eq (α := R) (HahnSeries.coeff (Γ := ℤ) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f) (↑a : ℤ) : R)
    (if LT.lt (α := ℤ) (↑a : ℤ) 0 then 0 else (coeff (Int.natAbs (↑a : ℤ)) : (a : R⟦X⟧) → R) f : R)
ofNat₁ :
  Eq (α := R) ((coeff a : (a : R⟦X⟧) → R) f : R)
    (if LT.lt (α := ℤ) (↑a : ℤ) 0 then 0 else (coeff (Int.natAbs (↑a : ℤ)) : (a : R⟦X⟧) → R) f : R)
ofNat₂ : Eq (α := R) ((coeff a : (a : R⟦X⟧) → R) f : R) ((coeff (Int.natAbs (↑a : ℤ)) : (a : R⟦X⟧) → R) f : R)
ofNat₃ ofNat₄ : Eq (α := R) ((coeff a : (a : R⟦X⟧) → R) f : R) ((coeff a : (a : R⟦X⟧) → R) f : R)
⊢ Eq (α := R) (HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f) (Int.ofNat a) : R)
    (if Int.ofNat a < 0 then 0 else (coeff (Int.ofNat a).natAbs : (a : R⟦X⟧) → R) f : R)

Tactic:
rw [Int.ofNat_eq_natCast, coeff_coe_powerSeries, if_neg (Int.natCast_nonneg _).not_gt,
      Int.natAbs_natCast]

Premises used: Int.ofNat_eq_natCast, LE.le.not_gt, Int.natAbs_natCast, if_neg, LaurentSeries.coeff_coe_powerSeries, Int.natCast_nonneg
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
a : ℕ
negSucc :
  Int.negSucc a ∉
    Set.image (α := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)
      (HahnSeries.support.{0, u_1} (R := R) ((RingEquiv.symm HahnSeries.toPowerSeries : (a : R⟦X⟧) → R⟦ℕ⟧) f))
⊢ Eq (α := R) (HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) f) (Int.negSucc a) : R)
    (if Int.negSucc a < 0 then 0 else (coeff (Int.negSucc a).natAbs : (a : R⟦X⟧) → R) f : R)

Tactic:
rw [ofPowerSeries_apply, embDomain_notin_image_support, if_pos (Int.negSucc_lt_zero _)]

Premises used: HahnSeries.embDomain_notin_image_support, Int.negSucc_lt_zero, if_pos, HahnSeries.ofPowerSeries_apply
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
a : ℕ
⊢ Int.negSucc a ∉
    Set.image (α := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)
      (HahnSeries.support.{0, u_1} (R := R) ((RingEquiv.symm HahnSeries.toPowerSeries : (a : R⟦X⟧) → R⟦ℕ⟧) f))

Tactic:
simp only [not_exists, RelEmbedding.coe_mk, Set.mem_image, not_and, Function.Embedding.coeFn_mk,
      Ne, toPowerSeries_symm_apply_coeff, mem_support, imp_true_iff,
      not_false_iff, reduceCtorEq]

Premises used: reduceCtorEq, Set.mem_image, not_exists, Ne, imp_true_iff, Function.Embedding.coeFn_mk, not_false_iff, not_and, HahnSeries.toPowerSeries_symm_apply_coeff, RelEmbedding.coe_mk, HahnSeries.mem_support
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
r : R
⊢ Eq (α := R⟦ℤ⟧) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) ((C : (a : R) → R⟦X⟧) r) : R⟦ℤ⟧)
    ((HahnSeries.C : (a : R) → R⟦ℤ⟧) r : R⟦ℤ⟧)

Tactic:
ofPowerSeries_C _

Premises used: HahnSeries.ofPowerSeries_C
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
⊢ Eq (α := R⟦ℤ⟧) (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) X : R⟦ℤ⟧)
    ((single 1 : (a : R) → R⟦ℤ⟧) 1 : R⟦ℤ⟧)

Tactic:
ofPowerSeries_X

Premises used: HahnSeries.ofPowerSeries_X
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
S : Type u_3
inst_1 : Semiring S
inst_2 : Module R S
r : R
x : S⟦X⟧
coeff :
  ∀ (x_1 : ℤ),
    HahnSeries.coeff (((ofPowerSeries ℤ S : S⟦X⟧ →+* S⟦ℤ⟧) : (a : S⟦X⟧) → S⟦ℤ⟧) (r • x)) x_1 =
      (HSMul.hSMul (β := S⟦ℤ⟧) r (((ofPowerSeries ℤ S : S⟦X⟧ →+* S⟦ℤ⟧) : (a : S⟦X⟧) → S⟦ℤ⟧) x : S⟦ℤ⟧)).coeff x_1
⊢ ((ofPowerSeries ℤ S : S⟦X⟧ →+* S⟦ℤ⟧) : (a : S⟦X⟧) → S⟦ℤ⟧) (r • x) =
    HSMul.hSMul (β := S⟦ℤ⟧) r (((ofPowerSeries ℤ S : S⟦X⟧ →+* S⟦ℤ⟧) : (a : S⟦X⟧) → S⟦ℤ⟧) x : S⟦ℤ⟧)

Tactic:
ext
-- Module: Mathlib.RingTheory.LaurentSeries
Goal:
R : Type u_1
inst : Semiring R
S : Type u_3
inst_1 : Semiring S
inst_2 : Module R S
r : R
x : S⟦X⟧
x_1 : ℤ
⊢ HahnSeries.coeff (((ofPowerSeries ℤ S : S⟦X⟧ →+* S⟦ℤ⟧) : (a : S⟦X⟧) → S⟦ℤ⟧) (r • x)) x_1 =
    (HSMul.hSMul (β := S⟦ℤ⟧) r (((ofPowerSeries ℤ S : S⟦X⟧ →+* S⟦ℤ⟧) : (a : S⟦X⟧) → S⟦ℤ⟧) x : S⟦ℤ⟧)).coeff x_1

Tactic:
simp [coeff_coe, coeff_smul, smul_ite]

Premises used: PowerSeries.coeff_coe, smul_ite, PowerSeries.coeff_smul