awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
this :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) : A)
refine_1 :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n) : A)
          ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₁ :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) (if i = n then 1 else 0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₂ :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) (0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
have refine_1₃ : ∀
  (this :
    Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A) (-(coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)),
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
Tactic: rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
this :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) : A)
refine_1 :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n) : A)
          ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₁ :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) (if i = n then 1 else 0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₂ :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) (0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₃ :
  ∀
    (this :
      Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (-(coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
have refine_1₄ : ∀
  (this :
    Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)),
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
Tactic: rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
this :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) : A)
refine_1 :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n) : A)
          ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₁ :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) (if i = n then 1 else 0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₂ :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) (0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₃ :
  ∀
    (this :
      Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (-(coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₄ :
  ∀
    (this :
      Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
have refine_1₅ : ∀ (this : Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)),
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
Tactic: rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
⊢ g = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
have this : HPow.hPow (α := A⟦X⟧) X n * (↑sorry.unit⁻¹ : A⟦X⟧) = (g * q + (↑r : A⟦X⟧)) * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: have := congr($(H.2) * ↑(H.isUnit_of_map_ne_zero hg).unit⁻¹)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
this : HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) = (g * q + (↑r : A⟦X⟧)) * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ g = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
have this₁ : HPow.hPow (α := A⟦X⟧) X n * (↑sorry.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑sorry.unit⁻¹ : A⟦X⟧) = g
Tactic: rw [add_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, ← sub_eq_iff_eq_add] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
this : HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) = g
⊢ g = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
have refine_2 : HPow.hPow (α := A⟦X⟧) X n * (↑sorry.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑sorry.unit⁻¹ : A⟦X⟧) = (↑f : A⟦X⟧) * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
this : HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) = g
refine_2 :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
refine_2₁ :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) =
    (↑(HPow.hPow (α := A[X]) Polynomial.X n - r) : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ g = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
have refine_2₂ : HPow.hPow (α := A⟦X⟧) X n * (↑sorry.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑sorry.unit⁻¹ : A⟦X⟧) =
  ((↑(HPow.hPow (α := A[X]) Polynomial.X n) : A⟦X⟧) - (↑r : A⟦X⟧)) * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
this : HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) = g
refine_2 :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
refine_2₁ :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) =
    (↑(HPow.hPow (α := A[X]) Polynomial.X n - r) : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
refine_2₂ :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) =
    ((↑(HPow.hPow (α := A[X]) Polynomial.X n) : A⟦X⟧) - (↑r : A⟦X⟧)) * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ g = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
have refine_2₃ : HPow.hPow (α := A⟦X⟧) X n * (↑sorry.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑sorry.unit⁻¹ : A⟦X⟧) =
  (HPow.hPow (α := A⟦X⟧) (↑Polynomial.X : A⟦X⟧) n - (↑r : A⟦X⟧)) * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
this : HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) = g
refine_2 :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
refine_2₁ :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) =
    (↑(HPow.hPow (α := A[X]) Polynomial.X n - r) : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
refine_2₂ :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) =
    ((↑(HPow.hPow (α := A[X]) Polynomial.X n) : A⟦X⟧) - (↑r : A⟦X⟧)) * (↑⋯.unit⁻¹ : A⟦X⟧)
refine_2₃ :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) =
    (HPow.hPow (α := A⟦X⟧) (↑Polynomial.X : A⟦X⟧) n - (↑r : A⟦X⟧)) * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ g = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
have refine_2₄ : HPow.hPow (α := A⟦X⟧) X n * (↑sorry.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑sorry.unit⁻¹ : A⟦X⟧) =
  (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
⊢ (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g (↑⋯.unit⁻¹ : A⟦X⟧)
    (HPow.hPow (α := A[X]) Polynomial.X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat -
      f)
have set : let n :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat;
∀
  (hn :
    n =
      (order.{u_1} (R := IsLocalRing.ResidueField A)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat),
  (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g (↑sorry.unit⁻¹ : A⟦X⟧) (HPow.hPow (α := A[X]) Polynomial.X n - f)
Tactic: set n := (g.map (IsLocalRing.residue A)).order.toNat with hn
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
hn :
  n =
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
⊢ (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g (↑⋯.unit⁻¹ : A⟦X⟧) (HPow.hPow (α := A[X]) Polynomial.X n - f)
have degree_lt : (HPow.hPow (α := A[X]) Polynomial.X n - f).degree <
  (↑(order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
          ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) : (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
            g)).toNat :
    WithBot ℕ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
hn :
  n =
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
degree_lt :
  (HPow.hPow (α := A[X]) Polynomial.X n - f).degree <
    (↑(order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
            ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) : (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
              g)).toNat :
      WithBot ℕ)
⊢ (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g (↑⋯.unit⁻¹ : A⟦X⟧) (HPow.hPow (α := A[X]) Polynomial.X n - f)
have eq_mul_add : HPow.hPow (α := A⟦X⟧) X n = g * (↑sorry.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
hn :
  n =
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
⊢ (HPow.hPow (α := A[X]) Polynomial.X n - f).degree <
    (↑(order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
            ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) : (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
              g)).toNat :
      WithBot ℕ)
have degree_lt : (HPow.hPow (α := A[X]) Polynomial.X n).degree = f.degree
Tactic: refine (Polynomial.degree_sub_lt ?_ (Polynomial.monic_X_pow n).ne_zero ?_).trans_eq (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
hn :
  n =
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
degree_lt : (HPow.hPow (α := A[X]) Polynomial.X n).degree = f.degree
⊢ (HPow.hPow (α := A[X]) Polynomial.X n - f).degree <
    (↑(order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
            ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) : (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
              g)).toNat :
      WithBot ℕ)
have degree_lt₁ : (HPow.hPow (α := A[X]) Polynomial.X n).leadingCoeff = f.leadingCoeff
Tactic: refine (Polynomial.degree_sub_lt ?_ (Polynomial.monic_X_pow n).ne_zero ?_).trans_eq (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
hn :
  n =
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
⊢ (HPow.hPow (α := A[X]) Polynomial.X n).degree = f.degree
have degree_lt : (HPow.hPow (α := A[X]) Polynomial.X n).degree =
  (↑((order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).lift
        sorry) :
    WithBot ℕ)
Tactic: simp_rw [H.degree_eq_coe_lift_order_map, Polynomial.degree_X_pow, n,
        ENat.lift_eq_toNat_of_lt_top]