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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h : ∀ (i : ℕ), Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) q : A) ((coeff i : (a : A⟦X⟧) → A) 0 : A)
⊢ q = 0

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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i : ℕ
⊢ Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) q : A) ((coeff i : (a : A⟦X⟧) → 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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i : ℕ
h :
  ∀ (k : ℕ),
    SModEq (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ k) ⊤) ((coeff i : (a : A⟦X⟧) → A) q : A) (0 : A)
⊢ Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) q : A) ((coeff i : (a : A⟦X⟧) → 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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i k : ℕ
h : Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
⊢ SModEq (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ k) ⊤) ((coeff i : (a : A⟦X⟧) → A) q : A) (0 : A)

Tactic:
rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]

Premises used: 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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i k : ℕ
⊢ Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)

Tactic:
this _ _

Premises used: Set.Mem
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i k : ℕ
⊢ Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)

Tactic:
exact this _ _
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
⊢ q = 0

Tactic:
have hq : q = 0 := by
      ext i
      refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
      rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]
      exact this _ _
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
hq : q = 0
⊢ r = 0

Tactic:
rw [hq, mul_zero, Eq.comm, Polynomial.coe_eq_zero_iff] at heq

Premises used: Polynomial.coe_eq_zero_iff, MulZeroClass.mul_zero, Eq.comm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
hq : q = 0
heq₁ : r = 0
⊢ ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)

Tactic:
rw [hq, mul_zero, Eq.comm, Polynomial.coe_eq_zero_iff] at heq

Premises used: Polynomial.coe_eq_zero_iff, MulZeroClass.mul_zero, Eq.comm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
hq : q = 0
heq₁ : r = 0
this₁ : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
⊢ q = 0

Tactic:
rw [hq, mul_zero, Eq.comm, Polynomial.coe_eq_zero_iff] at heq

Premises used: Polynomial.coe_eq_zero_iff, MulZeroClass.mul_zero, Eq.comm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : r = 0
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
hq : q = 0
⊢ q = 0 ∧ r = 0

Tactic:
⟨hq, heq⟩

Premises used: And.intro
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : r = 0
this : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
hq : q = 0
⊢ q = 0 ∧ r = 0

Tactic:
exact ⟨hq, heq⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
suffices : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
⊢ q = 0 ∧ r = 0

Tactic:
suffices ∀ k i, coeff i q ∈ I ^ k by
    have hq : q = 0 := by
      ext i
      refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
      rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]
      exact this _ _
    rw [hq, mul_zero, Eq.comm, Polynomial.coe_eq_zero_iff] at heq
    exact ⟨hq, heq⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
⊢ ∀ (i : ℕ), Membership.mem (α := A) (HPow.hPow (β := ℕ) I 0) ((coeff i : (a : A⟦X⟧) → A) q : 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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq : g * q = (↑r : A⟦X⟧)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
succ :
  ∀
    (heq :
      ((HPow.hPow (α := A⟦X⟧) X
                (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
              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) +
            (↑((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) :
              A⟦X⟧)) *
          q =
        (↑r : A⟦X⟧))
    (k : ℕ) (ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)) (i : ℕ),
    Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) q : A)
⊢ ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) q : A)

Tactic:
rw [g.eq_X_pow_mul_shift_add_trunc (g.map (Ideal.Quotient.mk I)).order.toNat] at heq

Premises used: Ideal.Quotient.mk, PowerSeries.eq_X_pow_mul_shift_add_trunc, PowerSeries.map, PowerSeries.order, ENat.toNat, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq :
  ((HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
          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) +
        (↑((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) :
          A⟦X⟧)) *
      q =
    (↑r : A⟦X⟧)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i : ℕ
inl :
  ∀ (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 + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
inr :
  ∀ (hi : (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat ≤ i),
    Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
⊢ Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)

Tactic:
rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi

Premises used: Ideal.Quotient.mk, PowerSeries.map, PowerSeries.order, ENat.toNat, lt_or_ge, DFunLike.coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq :
  ((HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
          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) +
        (↑((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) :
          A⟦X⟧)) *
      q =
    (↑r : A⟦X⟧)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
inl :
  Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        (((HPow.hPow (α := A⟦X⟧) X
                (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
              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) +
            (↑((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) :
              A⟦X⟧)) *
          q) :
      A)
⊢ Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)

Tactic:
rw [← heq, pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq :
  ((HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
          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) +
        (↑((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) :
          A⟦X⟧)) *
      q =
    (↑r : A⟦X⟧)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
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 * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        (((HPow.hPow (α := A⟦X⟧) X
                (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
              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) +
            (↑((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) :
              A⟦X⟧)) *
          q) :
      A)

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

Premises used: le_rfl, Set.Mem, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq :
  ((HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
          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) +
        (↑((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) :
          A⟦X⟧)) *
      q =
    (↑r : A⟦X⟧)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
inl :
  ∀ (j : ℕ) (hj : j ≤ i),
    Membership.mem (α := A) I
      ((coeff j : (a : A⟦X⟧) → A)
          ((HPow.hPow (α := A⟦X⟧) X
                (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
              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) +
            (↑((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) :
              A⟦X⟧)) :
        A)
⊢ Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        (((HPow.hPow (α := A⟦X⟧) X
                (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
              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) +
            (↑((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) :
              A⟦X⟧)) *
          q) :
      A)

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

Premises used: le_rfl, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq :
  ((HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
          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) +
        (↑((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) :
          A⟦X⟧)) *
      q =
    (↑r : A⟦X⟧)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
j : ℕ
hj : j ≤ i
inl :
  HAdd.hAdd (α := A) (β := A)
      ((coeff j : (a : A⟦X⟧) → A)
          (HPow.hPow (α := A⟦X⟧) X
              (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
            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) :
        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)
          j :
        A) ∈
    I
⊢ Membership.mem (α := A) I
    ((coeff j : (a : A⟦X⟧) → A)
        ((HPow.hPow (α := A⟦X⟧) X
              (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
            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) +
          (↑((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) :
            A⟦X⟧)) :
      A)

Tactic:
rw [map_add, Polynomial.coeff_coe]

Premises used: map_add, 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
inst_1 : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
heq :
  ((HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
          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) +
        (↑((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) :
          A⟦X⟧)) *
      q =
    (↑r : A⟦X⟧)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
i : ℕ
hi : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
j : ℕ
hj : j ≤ i
⊢ HAdd.hAdd (α := A) (β := A)
      ((coeff j : (a : A⟦X⟧) → A)
          (HPow.hPow (α := A⟦X⟧) X
              (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
            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) :
        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)
          j :
        A) ∈
    I

Tactic:
Ideal.add_mem _ ?_ (g.coeff_trunc_order_mem I j)

Premises used: Ideal.add_mem, _private.0.PowerSeries.coeff_trunc_order_mem