awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
x : R[X]
hx : HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0
this : x = (taylor (r - r) : (a : R[X]) → R[X]) x
rwa :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r - r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₁ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r + -r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₂ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor r : (a : R[X]) → R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x) : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₃ :
  ∀
    (hx :
      Eq (α := R[X])
        ((taylor r : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) p) : R[X])
        (0 : R[X]))
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₄ :
  ∀ (hx : HMul.hMul (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) p = 0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
⊢ x = 0
have rwa₅ : ∀ (hx : Eq (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) (0 : R[X]))
  (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
Tactic: rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
    LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
    LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
x : R[X]
hx : HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0
this : x = (taylor (r - r) : (a : R[X]) → R[X]) x
rwa :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r - r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₁ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r + -r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₂ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor r : (a : R[X]) → R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x) : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₃ :
  ∀
    (hx :
      Eq (α := R[X])
        ((taylor r : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) p) : R[X])
        (0 : R[X]))
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₄ :
  ∀ (hx : HMul.hMul (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) p = 0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₅ :
  ∀ (hx : Eq (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) (0 : R[X]))
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
⊢ x = 0
have rwa₆ : ∀ (hx : x = 0) (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
Tactic: rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
    LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
    LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
have rw : Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
  ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
Tactic: rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
rw :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
have rw₁ : Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
  (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
Tactic: rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
rw :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
have rw₂ : Eq (α := R⟮X⟯)
  ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯)
      (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
        ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)) :
    R⟮X⟯)
  (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
Tactic: rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
rw :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₂ :
  Eq (α := R⟮X⟯)
    ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯)
        (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
          ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)) :
      R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
have rw₃ : HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
  RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1
Tactic: rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
rw :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₂ :
  Eq (α := R⟮X⟯)
    ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯)
        (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
          ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)) :
      R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₃ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
have rw₄ : HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
Tactic: rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
rw :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₂ :
  Eq (α := R⟮X⟯)
    ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯)
        (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
          ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)) :
      R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₃ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1
rw₄ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
have rw₅ : HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) 1) : R⟮X⟯) =
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
Tactic: rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
rw :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₂ :
  Eq (α := R⟮X⟯)
    ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯)
        (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
          ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)) :
      R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₃ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1
rw₄ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
rw₅ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) 1) : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
have rw₆ : HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯) =
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
Tactic: rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
rw :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₂ :
  Eq (α := R⟮X⟯)
    ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯)
        (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
          ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)) :
      R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₃ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1
rw₄ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
rw₅ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) 1) : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
rw₆ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
have rw₇ : HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
    (1 : R⟮X⟯) =
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯) (1 : R⟮X⟯)
Tactic: rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
⊢ (laurent r : (a : R⟮X⟯) → R⟮X⟯) X = HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) X ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
have rw : (laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X) =
  HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
    ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
Tactic: rw [← algebraMap_X, laurent_algebraMap, taylor_X, map_add, algebraMap_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
rw :
  (laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
⊢ (laurent r : (a : R⟮X⟯) → R⟮X⟯) X = HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) X ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
have rw₁ : (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) Polynomial.X) =
  HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
    ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
Tactic: rw [← algebraMap_X, laurent_algebraMap, taylor_X, map_add, algebraMap_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
rw :
  (laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₁ :
  (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
⊢ (laurent r : (a : R⟮X⟯) → R⟮X⟯) X = HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) X ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
have rw₂ : (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯)
    (HAdd.hAdd (α := R[X]) (β := R[X]) Polynomial.X ((Polynomial.C : (a : R) → R[X]) r : R[X])) =
  HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
    ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
Tactic: rw [← algebraMap_X, laurent_algebraMap, taylor_X, map_add, algebraMap_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
rw :
  (laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₁ :
  (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₂ :
  (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯)
      (HAdd.hAdd (α := R[X]) (β := R[X]) Polynomial.X ((Polynomial.C : (a : R) → R[X]) r : R[X])) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
⊢ (laurent r : (a : R⟮X⟯) → R⟮X⟯) X = HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) X ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
have rw₃ : HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) r) : R⟮X⟯) =
  HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
    ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
Tactic: rw [← algebraMap_X, laurent_algebraMap, taylor_X, map_add, algebraMap_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
rw :
  (laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₁ :
  (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₂ :
  (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯)
      (HAdd.hAdd (α := R[X]) (β := R[X]) Polynomial.X ((Polynomial.C : (a : R) → R[X]) r : R[X])) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₃ :
  HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) r) : R⟮X⟯) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
⊢ (laurent r : (a : R⟮X⟯) → R⟮X⟯) X = HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) X ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
have rw₄ : HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
    ((C : (a : R) → R⟮X⟯) r : R⟮X⟯) =
  HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
    ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
Tactic: rw [← algebraMap_X, laurent_algebraMap, taylor_X, map_add, algebraMap_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
x : R
⊢ Eq (α := R⟮X⟯) ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((C : (a : R) → R⟮X⟯) x) : R⟮X⟯) ((C : (a : R) → R⟮X⟯) x : R⟮X⟯)
have rw : Eq (α := R⟮X⟯)
  ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x)) :
    R⟮X⟯)
  ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
Tactic: rw [← algebraMap_C, laurent_algebraMap, taylor_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
x : R
rw :
  Eq (α := R⟮X⟯)
    ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x)) :
      R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((C : (a : R) → R⟮X⟯) x) : R⟮X⟯) ((C : (a : R) → R⟮X⟯) x : R⟮X⟯)
have rw₁ : Eq (α := R⟮X⟯)
  ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) ((Polynomial.C : (a : R) → R[X]) x)) :
    R⟮X⟯)
  ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
Tactic: rw [← algebraMap_C, laurent_algebraMap, taylor_C]