awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ LT.lt (α := WithBot ℕ) ⊥
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)

Tactic:
WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ LT.lt (α := WithBot ℕ) ⊥
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)

Tactic:
exact WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ 0 = g * 0 + (↑0 : A⟦X⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
H : f.IsWeierstrassDivisionAt g q r I
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ f = g * q + (↑r : A⟦X⟧)

Tactic:
replace H := H.2
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f = g * q + (↑r : A⟦X⟧)
⊢ f - (↑r : A⟦X⟧) = g * q

Tactic:
rw [← sub_eq_iff_eq_add] at H

Premises used: sub_eq_iff_eq_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
rw : Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (g * q) : A)
⊢ Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (f - (↑r : A⟦X⟧)) : A)

Tactic:
rw [H]
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
⊢ Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (g * q) : A)

Tactic:
coeff_mul_mem_ideal_of_coeff_left_mem_ideal i (fun j hj ↦ ?_) i le_rfl

Premises used: le_rfl, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
refine : ∀ (j : ℕ) (hj : j ≤ i), Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
⊢ Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (g * q) : A)

Tactic:
refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal i (fun j hj ↦ ?_) i le_rfl

Premises used: le_rfl, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
j : ℕ
hj : j ≤ i
⊢ Eq (α := A ⧸ I)
    ((coeff j : (a : (A ⧸ I)⟦X⟧) → A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g) : A ⧸ I) (0 : A ⧸ I)

Tactic:
have := coeff_of_lt_order_toNat _ (lt_of_le_of_lt hj hi)
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
H : f - (↑r : A⟦X⟧) = g * q
j : ℕ
hj : j ≤ i
this :
  Eq (α := A ⧸ I)
    ((coeff j : (a : (A ⧸ I)⟦X⟧) → A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g) : A ⧸ I) (0 : A ⧸ I)
rwa :
  ∀
    (this :
      Eq (α := A ⧸ I) ((Ideal.Quotient.mk I : (a : A) → A ⧸ I) ((coeff j : (a : A⟦X⟧) → A) g) : A ⧸ I) (0 : A ⧸ I)),
    Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
rwa₁ :
  ∀
    (this :
      Membership.mem (α := A) (γ := Ideal A) (RingHom.ker (F := A →+* A ⧸ I) (Ideal.Quotient.mk I))
        ((coeff j : (a : A⟦X⟧) → A) g : A)),
    Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
rwa₂ rwa₃ rwa₄ rwa₅ :
  ∀ (this : Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)),
    Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)
⊢ Membership.mem (α := A) I ((coeff j : (a : A⟦X⟧) → A) g : A)

Tactic:
rwa [coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at this

Premises used: RingHom.mem_ker, PowerSeries.coeff_map, Ideal.mk_ker
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
rw : g * q + (↑r : A⟦X⟧) + (g * q' + (↑r' : A⟦X⟧)) = g * (q + q') + ((↑r : A⟦X⟧) + (↑r' : A⟦X⟧))
⊢ f + f' = g * (q + q') + (↑(r + r') : A⟦X⟧)

Tactic:
rw [H.eq_mul_add, H'.eq_mul_add, Polynomial.coe_add]

Premises used: PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, Polynomial.coe_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
⊢ g * q + (↑r : A⟦X⟧) + (g * q' + (↑r' : A⟦X⟧)) = g * (q + q') + ((↑r : A⟦X⟧) + (↑r' : A⟦X⟧))

Tactic:
ring
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
H : f.IsWeierstrassDivisionAt g q r I
a : A
⊢ a • f = g * a • q + (↑(a • r) : A⟦X⟧)

Tactic:
simp [H.eq_mul_add, Algebra.smul_def, mul_add, mul_left_comm]

Premises used: PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, mul_left_comm, Algebra.smul_def, mul_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
inst_1 : IsLocalRing A
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⟧)
rw :
  ((coeff
            (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 :
          (a : A⟦X⟧) → A)
        g :
      A) ∉
    IsLocalRing.maximalIdeal A
⊢ g.IsWeierstrassDivisor

Tactic:
rw [IsWeierstrassDivisor, IsWeierstrassDivisorAt, ← IsLocalRing.notMem_maximalIdeal]

Premises used: IsLocalRing.notMem_maximalIdeal, PowerSeries.IsWeierstrassDivisor, PowerSeries.IsWeierstrassDivisorAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
inst_1 : IsLocalRing A
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⟧)
⊢ Ne (α := IsLocalRing.ResidueField A)
    ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)

Tactic:
have h := coeff_order hg
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
inst_1 : IsLocalRing A
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 :
  Ne (α := IsLocalRing.ResidueField A)
    ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
contrapose :
  ∀
    (h :
      Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        ((coeff
                (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 :
              (a : A⟦X⟧) → A)
            g :
          A)),
    Eq (α := IsLocalRing.ResidueField A)
      ((coeff
              (order.{u_1} (R := IsLocalRing.ResidueField A)
                  ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
            (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
        IsLocalRing.ResidueField A)
      (0 : IsLocalRing.ResidueField A)
⊢ ((coeff
            (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 :
          (a : A⟦X⟧) → A)
        g :
      A) ∉
    IsLocalRing.maximalIdeal A

Tactic:
contrapose h
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
inst_1 : IsLocalRing A
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 :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff
            (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 :
          (a : A⟦X⟧) → A)
        g :
      A)
rwa :
  Eq (α := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A)
        ((coeff
              (order.{u_1} (R := IsLocalRing.ResidueField A)
                  ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
            (a : A⟦X⟧) → A)
          g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
rwa₁ rwa₂ rwa₃ rwa₄ :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : A⟦X⟧) → A)
        g :
      A)
⊢ Eq (α := IsLocalRing.ResidueField A)
    ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)

Tactic:
rwa [coeff_map, IsLocalRing.residue_eq_zero_iff]

Premises used: IsLocalRing.residue_eq_zero_iff, PowerSeries.coeff_map
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
hI : I ≠ ⊤
rwa : 1 ∉ I
rwa₁ rwa₂ rwa₃ rwa₄ : I ≠ ⊤
⊢ ((constantCoeff : (a : A⟦X⟧) → A) 1 : A) ∉ I

Tactic:
rwa [constantCoeff_one, ← Ideal.ne_top_iff_one]

Premises used: Ideal.ne_top_iff_one, PowerSeries.constantCoeff_one
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
hI : I ≠ ⊤
⊢ (↑g : A⟦X⟧) = (↑g : A⟦X⟧) * 1

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
hI : I ≠ ⊤
⊢ g.natDegree =
    ENat.toNat (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧)))

Tactic:
have : g.natDegree = _ := congr(ENat.toNat $(H.coe_natDegree_eq_order_map g 1
    (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one]) (by simp)))
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
hI : I ≠ ⊤
this :
  g.natDegree =
    ENat.toNat (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧)))
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt I

Tactic:
simp [IsWeierstrassDivisorAt, ← this, H.monic.leadingCoeff]

Premises used: Polynomial.IsDistinguishedAt.monic, Polynomial.Monic.leadingCoeff, PowerSeries.IsWeierstrassDivisorAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsHausdorff I A
inl : ∀ (H : g.IsDistinguishedAt ⊤) [IsHausdorff (R := A) ⊤ A], (↑g : A⟦X⟧).IsWeierstrassDivisorAt ⊤
inr : ∀ (hI : I ≠ ⊤), (↑g : A⟦X⟧).IsWeierstrassDivisorAt I
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt I

Tactic:
rcases eq_or_ne I ⊤ with rfl | hI

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
H : g.IsDistinguishedAt ⊤
inst_1 : IsHausdorff (R := A) ⊤ A
⊢ Subsingleton A

Tactic:
have := ‹IsHausdorff ⊤ A›.subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
H : g.IsDistinguishedAt ⊤
inst_1 : IsHausdorff (R := A) ⊤ A
this : Subsingleton A
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt ⊤

Tactic:
isUnit_of_subsingleton _

Premises used: isUnit_of_subsingleton, PowerSeries.IsWeierstrassDivisorAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
H : g.IsDistinguishedAt ⊤
inst_1 : IsHausdorff (R := A) ⊤ A
this : Subsingleton A
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt ⊤

Tactic:
exact isUnit_of_subsingleton _

Premises used: isUnit_of_subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsHausdorff I A
hI : I ≠ ⊤
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt I

Tactic:
H.isWeierstrassDivisorAt hI

Premises used: Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsHausdorff I A
hI : I ≠ ⊤
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt I

Tactic:
exact H.isWeierstrassDivisorAt hI

Premises used: Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
rw :
  Membership.mem (α := A) I
    (if i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat then
        (coeff i : (a : A⟦X⟧) → A) g
      else 0 :
      A)
⊢ Polynomial.coeff
      ((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
          (a : A⟦X⟧) → A[X])
        g)
      i ∈
    I

Tactic:
rw [coeff_trunc]

Premises used: PowerSeries.coeff_trunc
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
pos :
  ∀ (h : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) g : A)
neg : ∀ (h : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat), 0 ∈ I
⊢ Membership.mem (α := A) I
    (if i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat then
        (coeff i : (a : A⟦X⟧) → A) g
      else 0 :
      A)

Tactic:
split_ifs with h
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
h : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) g : A)

Tactic:
simpa [← RingHom.mem_ker] using coeff_of_lt_order_toNat _ h

Premises used: PowerSeries.coeff_of_lt_order_toNat, RingHom.mem_ker
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
h : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ 0 ∈ I

Tactic:
zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
h : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ 0 ∈ I

Tactic:
exact zero_mem _

Premises used: ZeroMemClass.zero_mem
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
⊢ IsUnit.{u_1} (M := A⟦X⟧)
    (mk fun (i : ℕ) ↦
      (coeff (i + (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
          (a : A⟦X⟧) → A)
        g)

Tactic:
simpa [isUnit_iff_constantCoeff]

Premises used: PowerSeries.isUnit_iff_constantCoeff
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ Membership.mem (α := A) (HPow.hPow (β := ℕ) I 0) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f 0) : A)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k : ℕ
hq :
  ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
succ :
  Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (H.seq f k +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    (f - g * H.seq f k)) *
                (↑⋯.unit⁻¹ : A⟦X⟧))) :
      A)
⊢ Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f (k + 1)) : A)

Tactic:
rw [seq]

Premises used: PowerSeries.IsWeierstrassDivisorAt.seq
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k : ℕ
hq :
  ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
succ :
  let q := H.seq f k;
  ∀
    (hq :
      ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
        Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * q) : A)),
    Membership.mem (α := A) (I ^ (k + 1))
      ((coeff i : (a : A⟦X⟧) → A)
          (f -
            g *
              (q +
                (mk fun (i : ℕ) ↦
                    (coeff
                          (i +
                            (order.{u_1} (R := A ⧸ I)
                                ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                        (a : A⟦X⟧) → A)
                      (f - g * q)) *
                  (↑⋯.unit⁻¹ : A⟦X⟧))) :
        A)
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (H.seq f k +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    (f - g * H.seq f k)) *
                (↑⋯.unit⁻¹ : A⟦X⟧))) :
      A)

Tactic:
set q := H.seq f k

Premises used: PowerSeries.IsWeierstrassDivisorAt.seq
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
q : A⟦X⟧ := H.seq f k
hq :
  ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * q) : A)
succ :
  let s := f - g * q;
  ∀
    (hq :
      ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
        Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)),
    Membership.mem (α := A) (I ^ (k + 1))
      ((coeff i : (a : A⟦X⟧) → A)
          (f -
            g *
              (q +
                (mk fun (i : ℕ) ↦
                    (coeff
                          (i +
                            (order.{u_1} (R := A ⧸ I)
                                ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                        (a : A⟦X⟧) → A)
                      s) *
                  (↑⋯.unit⁻¹ : A⟦X⟧))) :
        A)
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (q +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    (f - g * q)) *
                (↑⋯.unit⁻¹ : A⟦X⟧))) :
      A)

Tactic:
set s := f - g * q
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
hq :
  ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)
⊢ let n := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat;
  i ≥ n

Tactic:
set n := (g.map (Ideal.Quotient.mk I)).order.toNat

Premises used: Ideal.Quotient.mk, PowerSeries.map, PowerSeries.order, ENat.toNat, DFunLike.coe