awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟦ℤ⟧) =
    (single (-order z) : (a : R) → R⟦ℤ⟧) 1 * z
have 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
Tactic: rw [mul_comm _ z]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
have 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⟦ℤ⟧)
Tactic: refine congr rfl ?_
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : 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⟦ℤ⟧)
have neg : order z ≤ 0
Tactic: rw [ofPowerSeries_X_pow, Int.ofNat_natAbs_of_nonpos]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
x y : R⟦X⟧
⊢ 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
have rw : x = y → ∃ (c : ↥(Submonoid.powers PowerSeries.X)), (↑c : R⟦X⟧) * x = (↑c : R⟦X⟧) * y
Tactic: rw [coe_algebraMap, ofPowerSeries_injective.eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
i : ℤ
⊢ 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)
have 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)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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)
⊢ 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)
have 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)
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
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)
have 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)
Tactic: rw [Int.ofNat_eq_natCast, coeff_coe_powerSeries, if_neg (Int.natCast_nonneg _).not_gt,
      Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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)
⊢ 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)
have 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)
Tactic: rw [Int.ofNat_eq_natCast, coeff_coe_powerSeries, if_neg (Int.natCast_nonneg _).not_gt,
      Int.natAbs_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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)
⊢ 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)
have ofNat₂ : Eq (α := R) ((coeff a : (a : R⟦X⟧) → R) f : R) ((coeff (Int.natAbs (↑a : ℤ)) : (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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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)
⊢ 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)
have ofNat₃ : Eq (α := R) ((coeff a : (a : R⟦X⟧) → R) f : R) ((coeff a : (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]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
f : R⟦X⟧
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)
have negSucc : Int.negSucc a ∉
  Set.image (α := ℕ)
    (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := sorry } sorry) :
      (a : ℕ) → ℤ)
    (HahnSeries.support.{0, u_1} (R := R) ((RingEquiv.symm HahnSeries.toPowerSeries : (a : R⟦X⟧) → R⟦ℕ⟧) f))
Tactic: rw [ofPowerSeries_apply, embDomain_notin_image_support, if_pos (Int.negSucc_lt_zero _)]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟧
⊢ ((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⟦ℤ⟧)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
F : Type u
inst : Field F
p q : F[X]
f g : F⟮X⟯
⊢ FaithfulSMul.{u, u} F[X] F⸨X⸩
have refine : Function.Injective.{u + 1, u + 1} (α := F[X]) (β := F⸨X⸩) (⇑(algebraMap F[X] F⸨X⸩) : (a : F[X]) → F⸨X⸩)
Tactic: refine (faithfulSMul_iff_algebraMap_injective F[X] F⸨X⸩).mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw : (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
  HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw₁ : (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
  HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₁ :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw₂ : ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
  HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₁ :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₂ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw₃ : ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
  (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₁ :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₂ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₃ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw₄ : ((single (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
  (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ))⁻¹
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₁ :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₂ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₃ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₄ :
  ((single (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ))⁻¹
rw₅ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw₆ : (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
  HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ)
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₁ :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₂ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₃ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₄ :
  ((single (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ))⁻¹
rw₅ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₆ :
  (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ)
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw₇ : (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
  HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (n + (↑1 : ℕ))
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₁ :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₂ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₃ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₄ :
  ((single (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ))⁻¹
rw₅ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₆ :
  (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ)
rw₇ :
  (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (n + (↑1 : ℕ))
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw₈ : HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (n + (↑1 : ℕ)) =
  HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (n + (↑1 : ℕ))
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
F : Type u
inst : Field F
n_1 : ℤ
n : ℕ
rw :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₁ :
  (single (-(↑(n + (↑1 : ℕ)) : ℤ)) : (a : F) → F⟦ℤ⟧) 1⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₂ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (-(↑(n + (↑1 : ℕ)) : ℤ))
rw₃ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₄ :
  ((single (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑(↑1 : ℕ) : ℕ)) : ℤ))⁻¹
rw₅ :
  ((single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1)⁻¹ =
    (HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ))⁻¹
rw₆ :
  (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (↑(n + (↑1 : ℕ)) : ℤ)
rw₇ :
  (single (↑(n + (↑1 : ℕ)) : ℤ) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (n + (↑1 : ℕ))
rw₈ :
  HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (n + (↑1 : ℕ)) =
    HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1⁻¹) (n + (↑1 : ℕ))
⊢ (single (-(↑(n + 1) : ℤ)) : (a : F) → F⟦ℤ⟧) 1 =
    HPow.hPow (α := F⟦ℤ⟧) (β := ℤ) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (-(↑(n + 1) : ℤ))
have rw₉ : HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (n + (↑1 : ℕ)) =
  HPow.hPow (α := F⟦ℤ⟧) ((single 1 : (a : F) → F⟦ℤ⟧) 1) (n + (↑1 : ℕ))
Tactic: rw [← Nat.cast_one, ← inv_one, ← HahnSeries.inv_single, zpow_neg,
      ← Nat.cast_one, Nat.cast_one,
      inv_inj, zpow_natCast, single_one_eq_pow, inv_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
⊢ Ne (α := Ideal K⟦X⟧) (Ideal.span {X}) ⊥
have rw : ¬Eq.{u_2 + 1} (α := K⟦X⟧) X 0
Tactic: rw [ne_eq, Ideal.span_singleton_eq_bot]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
P : K[X]
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑P : K⟦X⟧) :
      WithZero (Multiplicative ℤ))
have pos : ∀ (hP : P = 0),
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑P : K⟦X⟧) :
      WithZero (Multiplicative ℤ))
Tactic: by_cases hP : P = 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
P : K[X]
pos :
  ∀ (hP : P = 0),
    Eq (α := WithZero (Multiplicative ℤ))
      (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
            (a : K[X]) → WithZero (Multiplicative ℤ))
          P :
        WithZero (Multiplicative ℤ))
      (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
            (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
          (↑P : K⟦X⟧) :
        WithZero (Multiplicative ℤ))
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑P : K⟦X⟧) :
      WithZero (Multiplicative ℤ))
have neg : ∀ (hP : ¬P = 0),
  Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑P : K⟦X⟧) :
      WithZero (Multiplicative ℤ))
Tactic: by_cases hP : P = 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
P : K[X]
hP : P = 0
⊢ Eq (α := WithZero (Multiplicative ℤ))
    (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
          (a : K[X]) → WithZero (Multiplicative ℤ))
        P :
      WithZero (Multiplicative ℤ))
    (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) :
          (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
        (↑P : K⟦X⟧) :
      WithZero (Multiplicative ℤ))
have pos : Eq (α := WithZero (Multiplicative ℤ))
  (((intValuation (Polynomial.idealX K) : Valuation K[X] (WithZero (Multiplicative ℤ))) :
        (a : K[X]) → WithZero (Multiplicative ℤ))
      0 :
    WithZero (Multiplicative ℤ))
  (((intValuation (idealX K) : Valuation K⟦X⟧ (WithZero (Multiplicative ℤ))) : (a : K⟦X⟧) → WithZero (Multiplicative ℤ))
      (↑0 : K⟦X⟧) :
    WithZero (Multiplicative ℤ))
Tactic: rw [hP, Valuation.map_zero, Polynomial.coe_zero, Valuation.map_zero]