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 : 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 =
    (↑((order.{u_1} (R := IsLocalRing.ResidueField A)
              ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).lift
          ⋯) :
      WithBot ℕ)
⊢ (HPow.hPow (α := A[X]) Polynomial.X n).degree = f.degree
have degree_lt₁ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ)
  (↑((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]
-- 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).leadingCoeff = f.leadingCoeff
have degree_lt : 1 = f.leadingCoeff
Tactic: rw [(Polynomial.monic_X_pow n).leadingCoeff, H.isDistinguishedAt.monic.leadingCoeff]
-- 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 : 1 = f.leadingCoeff
⊢ (HPow.hPow (α := A[X]) Polynomial.X n).leadingCoeff = f.leadingCoeff
have degree_lt₁ : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rw [(Polynomial.monic_X_pow n).leadingCoeff, H.isDistinguishedAt.monic.leadingCoeff]
-- 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 = g * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
have eq_mul_add : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) * h * (↑sorry.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
Tactic: simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]
-- 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
eq_mul_add :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * h * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
⊢ HPow.hPow (α := A⟦X⟧) X n = g * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
have eq_mul_add₁ : HPow.hPow (α := A⟦X⟧) X n =
  (↑f : A⟦X⟧) * (h * (↑sorry.unit⁻¹ : A⟦X⟧)) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
Tactic: simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]
-- 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
eq_mul_add :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * h * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₁ :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * (h * (↑⋯.unit⁻¹ : A⟦X⟧)) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
⊢ HPow.hPow (α := A⟦X⟧) X n = g * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
have eq_mul_add₂ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) * 1 + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
Tactic: simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]
-- 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
eq_mul_add :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * h * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₁ :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * (h * (↑⋯.unit⁻¹ : A⟦X⟧)) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₂ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) * 1 + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
⊢ HPow.hPow (α := A⟦X⟧) X n = g * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
have eq_mul_add₃ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
Tactic: simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]
-- 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
eq_mul_add :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * h * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₁ :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * (h * (↑⋯.unit⁻¹ : A⟦X⟧)) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₂ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) * 1 + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₃ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
⊢ HPow.hPow (α := A⟦X⟧) X n = g * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
have eq_mul_add₄ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + ((↑(HPow.hPow (α := A[X]) Polynomial.X n) : A⟦X⟧) - (↑f : A⟦X⟧))
Tactic: simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]
-- 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
eq_mul_add :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * h * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₁ :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * (h * (↑⋯.unit⁻¹ : A⟦X⟧)) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₂ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) * 1 + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₃ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₄ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + ((↑(HPow.hPow (α := A[X]) Polynomial.X n) : A⟦X⟧) - (↑f : A⟦X⟧))
⊢ HPow.hPow (α := A⟦X⟧) X n = g * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
have eq_mul_add₅ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + (HPow.hPow (α := A⟦X⟧) (↑Polynomial.X : A⟦X⟧) n - (↑f : A⟦X⟧))
Tactic: simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]
-- 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
eq_mul_add :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * h * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₁ :
  HPow.hPow (α := A⟦X⟧) X n =
    (↑f : A⟦X⟧) * (h * (↑⋯.unit⁻¹ : A⟦X⟧)) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₂ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) * 1 + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₃ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
eq_mul_add₄ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + ((↑(HPow.hPow (α := A[X]) Polynomial.X n) : A⟦X⟧) - (↑f : A⟦X⟧))
eq_mul_add₅ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + (HPow.hPow (α := A⟦X⟧) (↑Polynomial.X : A⟦X⟧) n - (↑f : A⟦X⟧))
⊢ HPow.hPow (α := A⟦X⟧) X n = g * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
have eq_mul_add₆ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + (HPow.hPow (α := A⟦X⟧) X n - (↑f : A⟦X⟧))
Tactic: simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
⊢ f = f' ∧ h = h'
have h1 : (↑sorry.unit⁻¹ : A⟦X⟧) = (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: obtain ⟨h1, h2⟩ := H.isWeierstrassDivision.elim H.map_ne_zero H2.isWeierstrassDivision
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : (↑⋯.unit⁻¹ : A⟦X⟧) = (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ f = f' ∧ h = h'
have h2 : 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 =
  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'
Tactic: obtain ⟨h1, h2⟩ := H.isWeierstrassDivision.elim H.map_ne_zero H2.isWeierstrassDivision
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : (↑⋯.unit⁻¹ : A⟦X⟧) = (↑⋯.unit⁻¹ : A⟦X⟧)
h2 :
  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 =
    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'
⊢ f = f' ∧ h = h'
have h1₁ : (↑sorry.unit : A⟦X⟧) = (↑sorry.unit : A⟦X⟧)
Tactic: rw [← Units.ext_iff, inv_inj, Units.ext_iff] at h1
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g : 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⟧)
⊢ ∃ (f : A[X]) (h : A⟦X⟧), g.IsWeierstrassFactorization f h
have obtain : ∀ (q : A⟦X⟧) (r : A[X])
  (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 q r),
  ∃ (f : A[X]) (h : A⟦X⟧), g.IsWeierstrassFactorization f h
Tactic: obtain ⟨q, r, H⟩ :=
    (X ^ (g.map (IsLocalRing.residue A)).order.toNat).exists_isWeierstrassDivision hg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ (g * g').weierstrassDistinguished hg =
    HMul.hMul (α := A[X]) (g.weierstrassDistinguished ⋯) (g'.weierstrassDistinguished ⋯)
have H : g.IsWeierstrassFactorization (g.weierstrassDistinguished sorry) (g.weierstrassUnit sorry)
Tactic: have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (g * g').weierstrassDistinguished hg =
    HMul.hMul (α := A[X]) (g.weierstrassDistinguished ⋯) (g'.weierstrassDistinguished ⋯)
have H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished sorry) (g'.weierstrassUnit sorry)
Tactic: have H' := g'.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
⊢ (g * g').weierstrassDistinguished hg =
    HMul.hMul (α := A[X]) (g.weierstrassDistinguished ⋯) (g'.weierstrassDistinguished ⋯)
have H'' : (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)
Tactic: have H'' := (g * g').isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯
have H : g.IsWeierstrassFactorization (g.weierstrassDistinguished sorry) (g.weierstrassUnit sorry)
Tactic: have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯
have H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished sorry) (g'.weierstrassUnit sorry)
Tactic: have H' := g'.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * g') :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : g'.IsWeierstrassFactorization (g'.weierstrassDistinguished ⋯) (g'.weierstrassUnit ⋯)
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯
have H'' : (g * g').IsWeierstrassFactorization ((g * g').weierstrassDistinguished hg) ((g * g').weierstrassUnit hg)
Tactic: have H'' := (g * g').isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯
have H : g.IsWeierstrassFactorization (g.weierstrassDistinguished sorry) (g.weierstrassUnit sorry)
Tactic: have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [Algebra.smul_def, h]))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯
have H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
Tactic: have H' := (a • g).isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯
have ha : Ne (α := IsLocalRing.ResidueField A)
  ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) a : IsLocalRing.ResidueField A)
  (0 : IsLocalRing.ResidueField A)
Tactic: have ha : IsLocalRing.residue A a ≠ 0 := fun h ↦ hg (by simp [Algebra.smul_def, h])
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯
have H : g.IsWeierstrassFactorization (g.weierstrassDistinguished sorry) (g.weierstrassUnit sorry)
Tactic: have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [Algebra.smul_def, h]))
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (a • g) :
      (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯
have H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
Tactic: have H' := (a • g).isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg