awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
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 (↑⋯.unit⁻¹ : A⟦X⟧) (HPow.hPow (α := A[X]) Polynomial.X n - f)
⊢ (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)

Tactic:
set n := (g.map (IsLocalRing.residue A)).order.toNat with hn

Premises used: IsLocalRing.residue, PowerSeries.map, PowerSeries.order, ENat.toNat, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
eq_mul_add : HPow.hPow (α := A⟦X⟧) X n = g * (↑⋯.unit⁻¹ : A⟦X⟧) + (↑(HPow.hPow (α := A[X]) Polynomial.X n - f) : A⟦X⟧)
⊢ (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g (↑⋯.unit⁻¹ : A⟦X⟧) (HPow.hPow (α := A[X]) Polynomial.X n - f)

Tactic:
constructor
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 =
    (↑(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:
simpa
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
degree_lt₁ : (HPow.hPow (α := A[X]) Polynomial.X n).leadingCoeff = f.leadingCoeff
⊢ (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:
refine (Polynomial.degree_sub_lt ?_ (Polynomial.monic_X_pow n).ne_zero ?_).trans_eq (by simpa)

Premises used: Polynomial.monic_X_pow, LT.lt.trans_eq, Polynomial.degree_sub_lt, Polynomial.Monic.ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
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
          ⋯) :
      WithBot ℕ)
degree_lt₂ :
  Eq (α := WithBot ℕ)
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)
    (↑((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

Tactic:
simp_rw [H.degree_eq_coe_lift_order_map, Polynomial.degree_X_pow, n,
        ENat.lift_eq_toNat_of_lt_top]

Premises used: Polynomial.degree_X_pow, ENat.lift_eq_toNat_of_lt_top, PowerSeries.IsWeierstrassFactorization.degree_eq_coe_lift_order_map
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
degree_lt₁ degree_lt₂ : Eq.{u_1 + 1} (α := A) 1 1
⊢ (HPow.hPow (α := A[X]) Polynomial.X n).leadingCoeff = f.leadingCoeff

Tactic:
rw [(Polynomial.monic_X_pow n).leadingCoeff, H.isDistinguishedAt.monic.leadingCoeff]

Premises used: Polynomial.monic_X_pow, Polynomial.IsDistinguishedAt.monic, PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt, Polynomial.Monic.leadingCoeff
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧))
eq_mul_add₆ : HPow.hPow (α := A⟦X⟧) X n = (↑f : A⟦X⟧) + (HPow.hPow (α := A⟦X⟧) 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⟧)

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]

Premises used: IsUnit.mul_val_inv, mul_assoc, Polynomial.coe_X, add_sub_cancel, PowerSeries.IsWeierstrassFactorizationAt.eq_mul, Polynomial.coe_sub, mul_one, Polynomial.coe_pow
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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'
⊢ (↑⋯.unit⁻¹ : A⟦X⟧) = (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
obtain ⟨h1, h2⟩ := H.isWeierstrassDivision.elim H.map_ne_zero H2.isWeierstrassDivision

Premises used: PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, PowerSeries.IsWeierstrassDivision.elim, PowerSeries.IsWeierstrassFactorization.map_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
⊢ 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

Premises used: PowerSeries.IsWeierstrassFactorization.isWeierstrassDivision, PowerSeries.IsWeierstrassDivision.elim, PowerSeries.IsWeierstrassFactorization.map_ne_zero
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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'
⊢ (↑⋯.unit : A⟦X⟧) = (↑⋯.unit : A⟦X⟧)

Tactic:
rw [← Units.ext_iff, inv_inj, Units.ext_iff] at h1

Premises used: Units.ext_iff, inv_inj
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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'
h1₁ : (↑⋯.unit : A⟦X⟧) = (↑⋯.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 =
    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:
rw [← Units.ext_iff, inv_inj, Units.ext_iff] at h1

Premises used: Units.ext_iff, inv_inj
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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'

Tactic:
simpa using h2
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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'

Tactic:
exact ⟨by simpa using h2, h1⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
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
⊢ ∃ (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

Premises used: IsLocalRing.residue, PowerSeries.X, PowerSeries.map, HPow.hPow, PowerSeries.exists_isWeierstrassDivision, PowerSeries.order, ENat.toNat, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
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:
⟨_, _, H.isWeierstrassFactorization hg⟩

Premises used: Exists.intro, PowerSeries.IsWeierstrassDivision.isWeierstrassFactorization
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
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:
exact ⟨_, _, H.isWeierstrassFactorization hg⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
⊢ g.IsWeierstrassFactorization (g.weierstrassDistinguished hg) (g.weierstrassUnit hg)

Tactic:
(g.exists_isWeierstrassFactorization hg).choose_spec.choose_spec

Premises used: Exists.choose_spec, PowerSeries.weierstrassDistinguished, PowerSeries.exists_isWeierstrassFactorization, PowerSeries.weierstrassUnit
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
⊢ (g.weierstrassDistinguished hg).IsDistinguishedAt (IsLocalRing.maximalIdeal A)

Tactic:
(g.exists_isWeierstrassFactorization hg).choose_spec.choose_spec.isDistinguishedAt

Premises used: Exists.choose_spec, PowerSeries.weierstrassDistinguished, PowerSeries.exists_isWeierstrassFactorization, PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
⊢ IsUnit (g.weierstrassUnit hg)

Tactic:
(g.exists_isWeierstrassFactorization hg).choose_spec.choose_spec.isUnit

Premises used: Exists.choose_spec, PowerSeries.exists_isWeierstrassFactorization, PowerSeries.IsWeierstrassFactorizationAt.isUnit, PowerSeries.weierstrassUnit
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
⊢ g = (↑(g.weierstrassDistinguished hg) : A⟦X⟧) * g.weierstrassUnit hg

Tactic:
(g.exists_isWeierstrassFactorization hg).choose_spec.choose_spec.eq_mul

Premises used: Exists.choose_spec, PowerSeries.weierstrassDistinguished, PowerSeries.exists_isWeierstrassFactorization, PowerSeries.weierstrassUnit, PowerSeries.IsWeierstrassFactorizationAt.eq_mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
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 = g.weierstrassDistinguished hg ∧ h = g.weierstrassUnit hg

Tactic:
H.elim (g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg)

Premises used: PowerSeries.IsWeierstrassFactorization.elim, PowerSeries.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g g' : A⟦X⟧
f : A[X]
h_1 : 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 :
  Eq (α := (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⟧)
⊢ Eq (α := (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⟧)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g g' : A⟦X⟧
f : A[X]
h_1 : 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 :
  Eq (α := (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⟧)
⊢ Eq (α := (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⟧)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 :
  Eq (α := (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⟧)
⊢ Eq (α := (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⟧)

Tactic:
simp [h]
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)

Tactic:
have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))