awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have neg : 0 = x.coeff n
Tactic: rw [ofPowerSeries_apply, embDomain_notin_range]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
neg : 0 = x.coeff n
⊢ HahnSeries.coeff (((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart) (n - order x) =
    x.coeff n
have neg₁ : n - order x ∉
  Set.range (ι := ℕ)
    (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
          { toFun := Nat.cast, inj' := sorry } sorry) :
      (a : ℕ) → ℤ)
Tactic: rw [ofPowerSeries_apply, embDomain_notin_range]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ 0 = x.coeff n
have neg : ∀ (h : 0 ≠ x.coeff n), order x ≤ n
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h : ¬order x ≤ n
⊢ n - order x ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)
have neg : ∀
  (h :
    Membership.mem (γ := Set ℤ)
      (Set.range (ι := ℕ)
        (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
              { toFun := Nat.cast, inj' := sorry } sorry) :
          (a : ℕ) → ℤ))
      (n - order x)),
  order x ≤ n
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
n : ℤ
h :
  Membership.mem (γ := Set ℤ)
    (Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := Nat.cast, inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ))
    (n - order x)
⊢ order x ≤ n
have h₁ : ∃ (y : ℕ), (↑y : ℤ) = n - order x
Tactic: simp only [Set.mem_range, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
⊢ ((ofPowerSeries ℤ R : R⟦X⟧ →+* R⟦ℤ⟧) : (a : R⟦X⟧) → R⟦ℤ⟧) x.powerSeriesPart =
    (single (-order x) : (a : R) → R⟦ℤ⟧) 1 * x
have refine : ((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: refine Eq.trans ?_ (congr rfl x.single_order_mul_powerSeriesPart)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : Semiring R
x : R⸨X⸩
⊢ ((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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟦ℤ⟧)
⊢ ((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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟦ℤ⟧)
⊢ ((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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟦ℤ⟧)
⊢ ((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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟦ℤ⟧)
⊢ ((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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟦ℤ⟧)
⊢ ((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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟦ℤ⟧)
⊢ ((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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: rw [← mul_assoc, single_mul_single, neg_add_cancel, mul_one, ← C_apply, C_one, one_mul]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⸩)
have refine_1 : HMul.hMul (α := R⸨X⸩) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1) ((single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1) = 1
Tactic: refine ⟨⟨single (n : ℤ) 1, single (-n : ℤ) 1, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ 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⸩)
have refine_2 : HMul.hMul (α := R⸨X⸩) ((single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1) = 1
Tactic: refine ⟨⟨single (n : ℤ) 1, single (-n : ℤ) 1, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ 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⸩)
have refine_3 : Eq (α := R⸨X⸩)
  ((↑{ val := (single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1, inv := (single (-(↑n : ℤ)) : (a : R) → R⟦ℤ⟧) 1, val_inv := sorry,
          inv_val := sorry } :
      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) sorry) :
        R⟦X⟧) :
    R⸨X⸩)
Tactic: refine ⟨⟨single (n : ℤ) 1, single (-n : ℤ) 1, ?_, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ 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⸩)
have 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⟦ℤ⟧)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
⊢ 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⟦ℤ⟧)
have refine_3 : Eq.{u_1 + 1} (α := R⸨X⸩) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1) ((single (↑n : ℤ) : (a : R) → R⟦ℤ⟧) 1)
Tactic: rw [ofPowerSeries_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
⊢ ∃ (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
have 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
Tactic: by_cases! h : 0 ≤ z.order
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
⊢ ∃ (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
have 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
Tactic: by_cases! h : 0 ≤ z.order
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
have 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
Tactic: refine ⟨⟨PowerSeries.X ^ Int.natAbs z.order * powerSeriesPart z, 1⟩, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : 0 ≤ order z
⊢ 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
have 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⟦ℤ⟧)
Tactic: simp only [map_one, mul_one, map_mul, coe_algebraMap, ofPowerSeries_X_pow,
        Submonoid.coe_one]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
R : Type u_1
inst : CommRing R
z : R⸨X⸩
h : 0 ≤ order 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⟦ℤ⟧)
have 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⟦ℤ⟧)
Tactic: rw [Int.natAbs_of_nonneg h, single_order_mul_powerSeriesPart]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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⟦ℤ⟧)
⊢ 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⟦ℤ⟧)
have pos₁ : z = z
Tactic: rw [Int.natAbs_of_nonneg h, single_order_mul_powerSeriesPart]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
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
have 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) sorry).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) sorry).1
Tactic: refine ⟨⟨powerSeriesPart z, PowerSeries.X ^ Int.natAbs z.order, ⟨_, 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
⊢ 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
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⟦ℤ⟧) =
  (single (-order z) : (a : R) → R⟦ℤ⟧) 1 * z
Tactic: simp only [coe_algebraMap, ofPowerSeries_powerSeriesPart]