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
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
rw :
  Membership.mem (α := A) (I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        ((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) ((coeff i : (a : A⟦X⟧) → A) (H.seq f (k + 1) - H.seq f k) : A)

Tactic:
rw [seq, add_sub_cancel_left]

Premises used: add_sub_cancel_left, 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 : ℕ
⊢ Membership.mem (α := A) (I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        ((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:
coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i

Premises used: PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal'
-- 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 : ℕ
refine :
  ∀ (i : ℕ),
    Membership.mem (α := A) (I ^ k)
      ((coeff i : (a : A⟦X⟧) → A)
          (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)) :
        A)
⊢ Membership.mem (α := A) (I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        ((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:
refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i

Premises used: PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal'
-- 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_1 i : ℕ
rw :
  Membership.mem (α := A) (I ^ k)
    ((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) :
      A)
⊢ Membership.mem (α := A) (I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        (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)) :
      A)

Tactic:
rw [coeff_mk]

Premises used: PowerSeries.coeff_mk
-- 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_1 i : ℕ
⊢ i + (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat ≥
    (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat

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 i_1 i : ℕ
⊢ Membership.mem (α := A) (I ^ k)
    ((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) :
      A)

Tactic:
exact H.coeff_seq_mem f k (by simp)

Premises used: PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem
-- 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⟧
⊢ H.seq f 0 = 0

Tactic:
rfl

Premises used: PowerSeries.IsWeierstrassDivisorAt.seq, rfl
-- 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⟧
simp_rw :
  0 +
      (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 * 0)) *
        (↑⋯.unit⁻¹ : 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)
          f) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
simp_rw₁ :
  0 +
      (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 - 0)) *
        (↑⋯.unit⁻¹ : 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)
          f) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
simp_rw₂ :
  (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 - 0)) *
      (↑⋯.unit⁻¹ : 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)
          f) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ H.seq f 1 =
    (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) *
      (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
simp_rw [seq, mul_zero, zero_add, sub_zero]

Premises used: sub_zero, zero_add, MulZeroClass.mul_zero, 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
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n : ℕ
base base₁ :
  Eq.{u_1 + 1} (α := A ⧸ HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    (Submodule.Quotient.mk ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m))
    (Submodule.Quotient.mk ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m))
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)

Tactic:
rw [SModEq.def]

Premises used: SModEq.def
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n_1 n : ℕ
hn : m ≤ n
ih :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))

Tactic:
ih.trans (SModEq.symm ?_)

Premises used: SModEq.symm, SModEq.trans
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n_1 n : ℕ
hn : m ≤ n
ih :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
succ :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))

Tactic:
refine ih.trans (SModEq.symm ?_)

Premises used: SModEq.symm, SModEq.trans
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n_1 n : ℕ
hn : m ≤ n
ih :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
succ : Membership.mem (α := A) (I ^ m) ((coeff i : (a : A⟦X⟧) → A) (H.seq f (n + 1) - H.seq f n) : A)
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)

Tactic:
rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← map_sub]

Premises used: map_sub, SModEq.sub_mem, smul_eq_mul, Ideal.mul_top
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n_1 n : ℕ
hn : m ≤ n
ih :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
⊢ Membership.mem (α := A) (I ^ m) ((coeff i : (a : A⟦X⟧) → A) (H.seq f (n + 1) - H.seq f n) : A)

Tactic:
Ideal.pow_le_pow_right hn (H.coeff_seq_succ_sub_seq_mem f n i)

Premises used: Set.Mem, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, Ideal.pow_le_pow_right
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n_1 n : ℕ
hn : m ≤ n
ih :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
⊢ Membership.mem (α := A) (I ^ m) ((coeff i : (a : A⟦X⟧) → A) (H.seq f (n + 1) - H.seq f n) : A)

Tactic:
exact Ideal.pow_le_pow_right hn (H.coeff_seq_succ_sub_seq_mem f n i)

Premises used: PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, Ideal.pow_le_pow_right
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n : ℕ
hn : m ≤ n
base :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
succ :
  ∀ (n : ℕ) (hn : m ≤ n)
    (ih :
      SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
        ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
        ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)),
    SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
      ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
      ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)

Tactic:
induction n, hn using Nat.le_induction with
      | base => rw [SModEq.def]
      | succ n hn ih =>
        refine ih.trans (SModEq.symm ?_)
        rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← map_sub]
        exact Ideal.pow_le_pow_right hn (H.coeff_seq_succ_sub_seq_mem f n i)

Premises used: map_sub, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, SModEq.def, SModEq.sub_mem, Ideal.pow_le_pow_right, smul_eq_mul, Ideal.mul_top
-- 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⟧
inst_1 : IsPrecomplete I A
i : ℕ
⊢ (coeff i : (a : A⟦X⟧) → A) (H.div f) = (↑(H.divCoeff f i) : A)

Tactic:
simp [div]

Premises used: PowerSeries.IsWeierstrassDivisorAt.div
-- 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⟧
inst_1 : IsPrecomplete I A
k i : ℕ
⊢ Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (H.div f - H.seq f k) : A)

Tactic:
simpa [coeff_div, SModEq.sub_mem] using ((H.divCoeff f i).2 k).symm

Premises used: SModEq.symm, SModEq.sub_mem, PowerSeries.IsWeierstrassDivisorAt.coeff_div, PowerSeries.IsWeierstrassDivisorAt.divCoeff, Subtype.property
-- 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⟧
inst_1 : IsAdicComplete I A
inl :
  ∀ (H : g.IsWeierstrassDivisorAt ⊤) [inst_2 : IsAdicComplete (R := A) ⊤ A],
    f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) ⊤
inr : ∀ (hI : I ≠ ⊤), f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) 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 f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst_1 : IsAdicComplete (R := A) ⊤ A
⊢ Subsingleton A

Tactic:
have := ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst_1 : IsAdicComplete (R := A) ⊤ A
this : Subsingleton A
inl : IsWeierstrassDivisionAt 0 g 0 0 ⊤
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) ⊤

Tactic:
rw [Subsingleton.elim f 0, Subsingleton.elim (H.div 0) 0, Subsingleton.elim (H.mod 0) 0]

Premises used: PowerSeries.IsWeierstrassDivisorAt.div, PowerSeries.IsWeierstrassDivisorAt.mod, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst_1 : IsAdicComplete (R := A) ⊤ A
this : Subsingleton A
⊢ IsWeierstrassDivisionAt 0 g 0 0 ⊤

Tactic:
g.isWeierstrassDivisionAt_zero _

Premises used: PowerSeries.isWeierstrassDivisionAt_zero
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst_1 : IsAdicComplete (R := A) ⊤ A
this : Subsingleton A
⊢ IsWeierstrassDivisionAt 0 g 0 0 ⊤

Tactic:
exact g.isWeierstrassDivisionAt_zero _

Premises used: PowerSeries.isWeierstrassDivisionAt_zero
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
inr :
  (H.mod f).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
inr₁ : f = g * H.div f + (↑(H.mod f) : A⟦X⟧)
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I

Tactic:
constructor
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
⊢ (H.mod f).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)

Tactic:
degree_trunc_lt _ _

Premises used: PowerSeries.degree_trunc_lt, PowerSeries.IsWeierstrassDivisorAt.mod
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
⊢ (H.mod f).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)

Tactic:
exact degree_trunc_lt _ _

Premises used: PowerSeries.degree_trunc_lt
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
inr :
  f - g * H.div f =
    (↑((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])
          (f - g * H.div f)) :
      A⟦X⟧)
⊢ f = g * H.div f + (↑(H.mod f) : A⟦X⟧)

Tactic:
rw [mod, add_comm, ← sub_eq_iff_eq_add]

Premises used: PowerSeries.IsWeierstrassDivisorAt.mod, add_comm, sub_eq_iff_eq_add
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
inr :
  ∀ (i : ℕ),
    Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A)
      ((coeff i : (a : A⟦X⟧) → A)
          (↑((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])
                (f - g * H.div f)) :
            A⟦X⟧) :
        A)
⊢ f - g * H.div f =
    (↑((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])
          (f - g * H.div f)) :
      A⟦X⟧)

Tactic:
ext i
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
inr :
  Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A)
    (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) (f - g * H.div f)
      else 0 :
      A)
⊢ Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A)
    ((coeff i : (a : A⟦X⟧) → A)
        (↑((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])
              (f - g * H.div f)) :
          A⟦X⟧) :
      A)

Tactic:
rw [Polynomial.coeff_coe, coeff_trunc]

Premises used: PowerSeries.coeff_trunc, Polynomial.coeff_coe
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
pos :
  ∀ (hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A)
neg :
  ∀ (hi : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A) (0 : A)
⊢ Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A)
    (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) (f - g * H.div f)
      else 0 :
      A)

Tactic:
split_ifs with hi
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A)

Tactic:
rfl
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A) (0 : A)

Tactic:
IsHausdorff.haus' (I := I) _ fun k ↦ ?_

Premises used: IsHausdorff.haus'
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
neg :
  ∀ (k : ℕ),
    SModEq (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ k) ⊤)
      ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A) (0 : A)
⊢ Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A) (0 : A)

Tactic:
refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_

Premises used: IsHausdorff.haus'
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
k : ℕ
⊢ f - g * H.div f = f - g * H.seq f k - g * (H.div f - H.seq f k)

Tactic:
ring
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
k : ℕ
neg :
  HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
      ((coeff i : (a : A⟦X⟧) → A) (g * (H.div f - H.seq f k)) : A) ∈
    I ^ k
⊢ SModEq (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ k) ⊤)
    ((coeff i : (a : A⟦X⟧) → A) (f - g * H.div f) : A) (0 : A)

Tactic:
rw [SModEq.zero, smul_eq_mul, Ideal.mul_top, show f - g * H.div f =
      f - g * (H.seq f k) - g * (H.div f - (H.seq f k)) by ring, map_sub]

Premises used: map_sub, SModEq.zero, smul_eq_mul, Ideal.mul_top
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
k : ℕ
⊢ HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
      ((coeff i : (a : A⟦X⟧) → A) (g * (H.div f - H.seq f k)) : A) ∈
    I ^ k

Tactic:
Ideal.sub_mem _ (H.coeff_seq_mem f k (not_lt.1 hi)) <|
      coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (H.coeff_div_sub_seq_mem f k) i

Premises used: PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal', Set.Mem, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, not_lt, Iff.mp, Ideal.sub_mem, PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem
-- 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⟧
inst_1 : IsAdicComplete I A
hI : I ≠ ⊤
i : ℕ
hi : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
k : ℕ
⊢ HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
      ((coeff i : (a : A⟦X⟧) → A) (g * (H.div f - H.seq f k)) : A) ∈
    I ^ k

Tactic:
exact Ideal.sub_mem _ (H.coeff_seq_mem f k (not_lt.1 hi)) <|
      coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (H.coeff_div_sub_seq_mem f k) i

Premises used: PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal', PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, not_lt, Iff.mp, Ideal.sub_mem, PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem