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 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 ℕ)
set :
  let n :=
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat;
  ∀ (H_1 : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r) (H1 : r.degree < (↑n : WithBot ℕ)),
    g.IsWeierstrassFactorization (HPow.hPow (α := A[X]) Polynomial.X n - r) (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ g.IsWeierstrassFactorization
    (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 -
      r)
    (↑⋯.unit⁻¹ : A⟦X⟧)

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

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 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
H1 : r.degree < (↑n : WithBot ℕ)
set :
  let f := HPow.hPow (α := A[X]) Polynomial.X n - r;
  g.IsWeierstrassFactorization f (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ g.IsWeierstrassFactorization (HPow.hPow (α := A[X]) Polynomial.X n - r) (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
set f := Polynomial.X ^ n - r

Premises used: Polynomial.X
-- 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_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
H1 : r.degree < (↑n : WithBot ℕ)
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
rwa rwa₁ rwa₂ rwa₃ : r.degree < (↑n : WithBot ℕ)
⊢ r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree

Tactic:
rwa [Polynomial.degree_X_pow]

Premises used: Polynomial.degree_X_pow
-- 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_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
H1 : r.degree < (↑n : WithBot ℕ)
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
⊢ r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree

Tactic:
replace H1 : r.degree < (Polynomial.X (R := A) ^ n).degree := by rwa [Polynomial.degree_X_pow]
-- 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_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
this : f.degree = (↑n : WithBot ℕ)
rw : WithBot.unbotD 0 (↑n : WithBot ℕ) = n
⊢ f.natDegree = n

Tactic:
rw [Polynomial.natDegree, this]

Premises used: Polynomial.natDegree
-- 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_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
this : f.degree = (↑n : WithBot ℕ)
⊢ WithBot.unbotD 0 (↑n : WithBot ℕ) = n

Tactic:
rfl
-- 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_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
suffices : f.degree = (↑n : WithBot ℕ)
⊢ f.natDegree = n

Tactic:
suffices f.degree = n by rw [Polynomial.natDegree, this]; rfl
-- 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_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
rw : (HPow.hPow (α := A[X]) Polynomial.X n).degree = (↑n : WithBot ℕ)
rw₁ rw₂ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
⊢ f.degree = (↑n : WithBot ℕ)

Tactic:
rw [Polynomial.degree_sub_eq_left_of_degree_lt H1, Polynomial.degree_X_pow]

Premises used: Polynomial.degree_X_pow, Polynomial.degree_sub_eq_left_of_degree_lt
-- 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_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
⊢ f.natDegree = n

Tactic:
have hfdeg : f.natDegree = n := by
    suffices f.degree = n by rw [Polynomial.natDegree, this]; rfl
    rw [Polynomial.degree_sub_eq_left_of_degree_lt H1, Polynomial.degree_X_pow]
-- 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_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.IsWeierstrassFactorization f (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
⟨⟨⟨fun {i} hi ↦ ?_⟩, .sub_of_left (Polynomial.monic_X_pow _) H1⟩, Units.isUnit _, ?_⟩

Premises used: Polynomial.monic_X_pow, PowerSeries.IsWeierstrassFactorizationAt.mk, Polynomial.IsDistinguishedAt.mk, Polynomial.IsWeaklyEisensteinAt.mk, Polynomial.Monic.sub_of_left, Units.isUnit
-- 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_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
refine_1 : ∀ {i : ℕ} (hi : i < f.natDegree), Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (f.coeff i)
refine_2 : g = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ g.IsWeierstrassFactorization f (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
refine ⟨⟨⟨fun {i} hi ↦ ?_⟩, .sub_of_left (Polynomial.monic_X_pow _) H1⟩, Units.isUnit _, ?_⟩
-- 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_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 < f.natDegree
⊢ i < n

Tactic:
rw [hfdeg] at hi
-- 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_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
refine_1 : Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (f.coeff i)

Tactic:
simp_rw [f, Polynomial.coeff_sub, Polynomial.coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff]

Premises used: neg_mem_iff, Polynomial.coeff_X_pow, Polynomial.coeff_sub, if_neg, zero_sub, LT.lt.ne
-- 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_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
⊢ Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) : A)

Tactic:
have := H.coeff_f_sub_r_mem hi
-- 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_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)
refine_1₅ refine_1₆ refine_1₇ refine_1₈ :
  ∀ (this : Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)),
    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

Premises used: neg_mem_iff, map_sub, PowerSeries.coeff_X_pow, if_neg, Polynomial.coeff_coe, zero_sub, LT.lt.ne
-- 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_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
⊢ HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) = (g * q + (↑r : A⟦X⟧)) * (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
have := congr($(H.2) * ↑(H.isUnit_of_map_ne_zero hg).unit⁻¹)
-- 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_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⟧)
⊢ HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) = g

Tactic:
rw [add_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, ← sub_eq_iff_eq_add] at this

Premises used: add_mul, IsUnit.mul_val_inv, mul_assoc, sub_eq_iff_eq_add, mul_one
-- 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_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⟧)
refine_2₄ :
  HPow.hPow (α := A⟦X⟧) X n * (↑⋯.unit⁻¹ : A⟦X⟧) - (↑r : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧) =
    (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ g = (↑f : A⟦X⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]

Premises used: Polynomial.coe_X, sub_mul, Polynomial.coe_sub, Polynomial.coe_pow