awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f f' g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
pos :
  ∀
    (h :
      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⟧)),
    IsWeierstrassDivisorAt.mod ⋯ (f + f') = IsWeierstrassDivisorAt.mod ⋯ f + IsWeierstrassDivisorAt.mod ⋯ f'
neg :
  ¬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⟧) →
    0 = HAdd.hAdd (α := A[X]) 0 0
⊢ (if 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⟧) then
      IsWeierstrassDivisorAt.mod ⋯ (f + f')
    else 0) =
    HAdd.hAdd (α := A[X])
      (if 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⟧) then
        IsWeierstrassDivisorAt.mod ⋯ f
      else 0)
      (if 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⟧) then
        IsWeierstrassDivisorAt.mod ⋯ f'
      else 0)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f f' g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  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⟧)
⊢ IsWeierstrassDivisorAt.mod ⋯ (f + f') = IsWeierstrassDivisorAt.mod ⋯ f + IsWeierstrassDivisorAt.mod ⋯ f'

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

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
a : A
f g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
pos :
  ∀
    (h :
      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⟧)),
    IsWeierstrassDivisorAt.mod ⋯ (a • f) = a • IsWeierstrassDivisorAt.mod ⋯ f
neg :
  ¬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⟧) →
    0 = HSMul.hSMul (β := A[X]) a 0
⊢ (if 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⟧) then
      IsWeierstrassDivisorAt.mod ⋯ (a • f)
    else 0) =
    HSMul.hSMul (β := A[X]) a
      (if 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⟧) then
        IsWeierstrassDivisorAt.mod ⋯ f
      else 0)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
a : A
f g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  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⟧)
⊢ IsWeierstrassDivisorAt.mod ⋯ (a • f) = a • IsWeierstrassDivisorAt.mod ⋯ f

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

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
pos :
  ∀
    (h :
      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⟧)),
    IsWeierstrassDivisorAt.mod ⋯ 0 = 0
neg :
  ¬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⟧) →
    Eq.{u_1 + 1} (α := A[X]) 0 0
⊢ Eq.{u_1 + 1} (α := A[X])
    (if 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⟧) then
      IsWeierstrassDivisorAt.mod ⋯ 0
    else 0)
    0

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  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⟧)
⊢ IsWeierstrassDivisorAt.mod ⋯ 0 = 0

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

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ Nontrivial.{u_1} (A ⧸ I)

Tactic:
have := Ideal.Quotient.nontrivial_iff.mpr hI
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
rw : ¬(↑(Polynomial.map (Ideal.Quotient.mk I) f) : (A ⧸ I)⟦X⟧) = 0
⊢ Ne (α := (A ⧸ I)⟦X⟧) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g : (A ⧸ I)⟦X⟧) (0 : (A ⧸ I)⟦X⟧)

Tactic:
rw [congr(map (Ideal.Quotient.mk I) $(H.eq_mul)), map_mul, ← Polynomial.polynomial_map_coe, ne_eq,
    (H.isUnit.map _).mul_left_eq_zero]

Premises used: IsUnit.mul_left_eq_zero, PowerSeries.IsWeierstrassFactorizationAt.isUnit, ne_eq, map_mul, IsUnit.map, Polynomial.polynomial_map_coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
⊢ ¬(↑(Polynomial.map (Ideal.Quotient.mk I) f) : (A ⧸ I)⟦X⟧) = 0

Tactic:
exact_mod_cast f.map_monic_ne_zero (f := Ideal.Quotient.mk I) H.isDistinguishedAt.monic

Premises used: Polynomial.IsDistinguishedAt.monic, Polynomial.map_monic_ne_zero, PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ f.degree =
    (↑((order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).lift ⋯) : WithBot ℕ)

Tactic:
H.isDistinguishedAt.degree_eq_coe_lift_order_map g h ?_ H.eq_mul

Premises used: Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, PowerSeries.IsWeierstrassFactorizationAt.eq_mul, PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
refine : ((constantCoeff : (a : A⟦X⟧) → A) h : A) ∉ I
⊢ f.degree =
    (↑((order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).lift ⋯) : WithBot ℕ)

Tactic:
refine H.isDistinguishedAt.degree_eq_coe_lift_order_map g h ?_ H.eq_mul

Premises used: Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, PowerSeries.IsWeierstrassFactorizationAt.eq_mul, PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
contrapose : ∀ (hI : Membership.mem (α := A) I ((constantCoeff : (a : A⟦X⟧) → A) h : A)), I = ⊤
⊢ ((constantCoeff : (a : A⟦X⟧) → A) h : A) ∉ I

Tactic:
contrapose hI
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : Membership.mem (α := A) I ((constantCoeff : (a : A⟦X⟧) → A) h : A)
⊢ I = ⊤

Tactic:
Ideal.eq_top_of_isUnit_mem _ hI (isUnit_iff_constantCoeff.1 H.isUnit)

Premises used: PowerSeries.isUnit_iff_constantCoeff, Ideal.eq_top_of_isUnit_mem, PowerSeries.IsWeierstrassFactorizationAt.isUnit, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : Membership.mem (α := A) I ((constantCoeff : (a : A⟦X⟧) → A) h : A)
⊢ I = ⊤

Tactic:
exact Ideal.eq_top_of_isUnit_mem _ hI (isUnit_iff_constantCoeff.1 H.isUnit)

Premises used: PowerSeries.isUnit_iff_constantCoeff, Ideal.eq_top_of_isUnit_mem, PowerSeries.IsWeierstrassFactorizationAt.isUnit, Iff.mp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
rw :
  WithBot.unbotD 0
      (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ) =
    (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ f.natDegree = (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat

Tactic:
rw [Polynomial.natDegree, H.degree_eq_coe_lift_order_map_of_ne_top hI,
    ENat.lift_eq_toNat_of_lt_top]

Premises used: ENat.lift_eq_toNat_of_lt_top, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, Polynomial.natDegree
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ WithBot.unbotD 0
      (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ) =
    (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat

Tactic:
WithBot.unbotD_coe _ _

Premises used: WithBot.unbotD_coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ WithBot.unbotD 0
      (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ) =
    (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat

Tactic:
exact WithBot.unbotD_coe _ _

Premises used: WithBot.unbotD_coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
inst_1 : IsAdicComplete I A
rw : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {(↑f : A⟦X⟧) * h})
rw₁ rw₂ : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {(↑f : A⟦X⟧)})
⊢ Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {g})

Tactic:
rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]

Premises used: Ideal.span_singleton_mul_right_unit, PowerSeries.IsWeierstrassFactorizationAt.isUnit, PowerSeries.IsWeierstrassFactorizationAt.eq_mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
inst_1 : IsAdicComplete I A
x : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})
rw : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧) * h}) (Ideal.span {(↑f : A⟦X⟧)})
rw₁ rw₂ : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {(↑f : A⟦X⟧)})
⊢ Eq (α := Ideal A⟦X⟧) (Ideal.span {g}) (Ideal.span {(↑f : A⟦X⟧)})

Tactic:
rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]

Premises used: Ideal.span_singleton_mul_right_unit, PowerSeries.IsWeierstrassFactorizationAt.isUnit, PowerSeries.IsWeierstrassFactorizationAt.eq_mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
inst_1 : IsAdicComplete I A
x : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})
⊢ Eq (α := HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {f}))
    ((H.algEquivQuotient.symm : (a : A⟦X⟧ ⧸ Ideal.span {g}) → A[X] ⧸ Ideal.span {f}) x :
      HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {f}))
    ((Ideal.Quotient.mk (Ideal.span {f}) : (a : A[X]) → A[X] ⧸ Ideal.span {f})
        ((⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑f : A⟦X⟧)}) → A[X])
          ((Ideal.quotientEquivAlgOfEq A ⋯ : (a : A⟦X⟧ ⧸ Ideal.span {g}) → A⟦X⟧ ⧸ Ideal.span {(↑f : A⟦X⟧)}) x)) :
      HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {f}))

Tactic:
simp [algEquivQuotient]

Premises used: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
rw : (↑f : A⟦X⟧) * h * ((↑f' : A⟦X⟧) * h') = (↑f : A⟦X⟧) * (↑f' : A⟦X⟧) * (h * h')
⊢ g * g' = (↑(f * f') : A⟦X⟧) * (h * h')

Tactic:
rw [H.eq_mul, H'.eq_mul, Polynomial.coe_mul]

Premises used: PowerSeries.IsWeierstrassFactorizationAt.eq_mul, Polynomial.coe_mul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ (↑f : A⟦X⟧) * h * ((↑f' : A⟦X⟧) * h') = (↑f : A⟦X⟧) * (↑f' : A⟦X⟧) * (h * h')

Tactic:
ring
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ (a • g).IsWeierstrassFactorizationAt f (a • h) I

Tactic:
⟨H.isDistinguishedAt, ?_, ?_⟩

Premises used: PowerSeries.IsWeierstrassFactorizationAt.mk, PowerSeries.IsWeierstrassFactorizationAt.isDistinguishedAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
refine_1 : IsUnit (a • h)
refine_2 : a • g = (↑f : A⟦X⟧) * a • h
⊢ (a • g).IsWeierstrassFactorizationAt f (a • h) I

Tactic:
refine ⟨H.isDistinguishedAt, ?_, ?_⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
refine_1 : IsUnit (HMul.hMul (α := A⟦X⟧) ((algebraMap A A⟦X⟧ : (a : A) → A⟦X⟧) a : A⟦X⟧) h)
⊢ IsUnit (a • h)

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ IsUnit (HMul.hMul (α := A⟦X⟧) ((algebraMap A A⟦X⟧ : (a : A) → A⟦X⟧) a : A⟦X⟧) h)

Tactic:
(ha.map _).mul H.isUnit

Premises used: IsUnit.mul, PowerSeries.IsWeierstrassFactorizationAt.isUnit, IsUnit.map
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ IsUnit (HMul.hMul (α := A⟦X⟧) ((algebraMap A A⟦X⟧ : (a : A) → A⟦X⟧) a : A⟦X⟧) h)

Tactic:
exact (ha.map _).mul H.isUnit

Premises used: IsUnit.mul, PowerSeries.IsWeierstrassFactorizationAt.isUnit, IsUnit.map
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ a • g = (↑f : A⟦X⟧) * a • h

Tactic:
simp [H.eq_mul]

Premises used: PowerSeries.IsWeierstrassFactorizationAt.eq_mul
-- 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
⊢ 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⟧)

Tactic:
H.map_ne_zero_of_ne_top (Ideal.IsMaximal.ne_top inferInstance)

Premises used: inferInstance, IsLocalRing.ResidueField, PowerSeries.IsWeierstrassFactorizationAt.map_ne_zero_of_ne_top, Ideal.IsMaximal.ne_top
-- 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
⊢ f.degree =
    (↑((order.{u_1} (R := IsLocalRing.ResidueField A)
              ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).lift
          ⋯) :
      WithBot ℕ)

Tactic:
H.degree_eq_coe_lift_order_map_of_ne_top (Ideal.IsMaximal.ne_top inferInstance)

Premises used: inferInstance, IsLocalRing.ResidueField, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, Ideal.IsMaximal.ne_top
-- 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
⊢ f.natDegree =
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat

Tactic:
H.natDegree_eq_toNat_order_map_of_ne_top (Ideal.IsMaximal.ne_top inferInstance)

Premises used: PowerSeries.IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top, inferInstance, IsLocalRing.ResidueField, Ideal.IsMaximal.ne_top
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 :
  (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
⊢ r.degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)

Tactic:
obtain ⟨H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat, H2⟩ := H

Premises used: IsLocalRing.residue, Polynomial.degree, 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 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 :
  (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
H1 :
  r.degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)
⊢ 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 =
    g * q + (↑r : A⟦X⟧)

Tactic:
obtain ⟨H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat, H2⟩ := H

Premises used: IsLocalRing.residue, Polynomial.degree, 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 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⟧)
H1 :
  r.degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)
H2 :
  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 =
    g * q + (↑r : A⟦X⟧)
⊢ let n :=
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat;
  r.degree < (↑n : WithBot ℕ)

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

Premises used: IsLocalRing.residue, PowerSeries.map, PowerSeries.order, ENat.toNat, DFunLike.coe