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 :
  ((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 :
  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) :
      A)
⊢ 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:
refine Ideal.add_mem _ ?_ (g.coeff_trunc_order_mem I j)

Premises used: Ideal.add_mem, _private.0.PowerSeries.coeff_trunc_order_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 :
  ((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 :
  Membership.mem (α := A) I
    (if (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat ≤ j then
        (coeff (j - (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
            (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)
              g)
      else 0 :
      A)
inl₁ : 0 ∈ 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) :
      A)

Tactic:
simp_rw [coeff_X_pow_mul', if_neg (lt_of_le_of_lt hj hi).not_ge, zero_mem]

Premises used: lt_of_le_of_lt, ZeroMemClass.zero_mem, LT.lt.not_ge, PowerSeries.coeff_X_pow_mul', if_neg
-- 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 : (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat ≤ i
⊢ LE.le (α := WithBot ℕ)
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
    (↑i : WithBot ℕ)

Tactic:
simpa
-- 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 : (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat ≤ i
inr : r.coeff i ∈ I ^ (k + 1)
inr₁ : 0 ∈ I ^ (k + 1)
⊢ Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)

Tactic:
simp_rw [Polynomial.coeff_coe,
        Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg (by simpa)), zero_mem]

Premises used: ZeroMemClass.zero_mem, Polynomial.coeff_coe, lt_of_lt_of_le, Polynomial.coeff_eq_zero_of_degree_lt
-- 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 : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)

Tactic:
have h1 : ∀ i, coeff i r ∈ I ^ (k + 1) := fun i ↦ by
      rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi
      · rw [← heq, pow_succ']
        refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal i (fun j hj ↦ ?_)
          (fun j _ ↦ ih j) i le_rfl
        rw [map_add, Polynomial.coeff_coe]
        refine Ideal.add_mem _ ?_ (g.coeff_trunc_order_mem I j)
        simp_rw [coeff_X_pow_mul', if_neg (lt_of_le_of_lt hj hi).not_ge, zero_mem]
      simp_rw [Polynomial.coeff_coe,
        Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg (by simpa)), 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
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)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
succ :
  ∀
    (heq :
      (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) *
            HPow.hPow (α := A⟦X⟧) X
              (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
          q =
        (↑r : A⟦X⟧) -
          (↑((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)
    (k : ℕ) (ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A))
    (h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : 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 [add_mul, mul_comm (X ^ _), ← eq_sub_iff_add_eq] at heq

Premises used: add_mul, eq_sub_iff_add_eq, PowerSeries.X, HPow.hPow, mul_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 :
  (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) *
        HPow.hPow (α := A⟦X⟧) X
          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
      q =
    (↑r : A⟦X⟧) -
      (↑((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
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
⊢ (↑⋯.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)
              g) *
          HPow.hPow (α := A⟦X⟧) X
            (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
        q) =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)

Tactic:
replace heq := congr(H.isUnit_shift.unit⁻¹ * $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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
heq :
  (↑⋯.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)
              g) *
          HPow.hPow (α := A⟦X⟧) X
            (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
        q) =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)
⊢ HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)

Tactic:
rw [← mul_assoc, ← mul_assoc, IsUnit.val_inv_mul, one_mul] at heq

Premises used: mul_assoc, IsUnit.val_inv_mul, one_mul
-- 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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
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 *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)
i : ℕ
succ :
  Membership.mem (α := A) (I ^ (k + 1))
    ((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)
        ((↑⋯.unit⁻¹ : A⟦X⟧) *
          ((↑r : A⟦X⟧) -
            (↑((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) q : A)

Tactic:
rw [← coeff_X_pow_mul _ (g.map (Ideal.Quotient.mk I)).order.toNat i, heq]

Premises used: Ideal.Quotient.mk, PowerSeries.map, PowerSeries.order, ENat.toNat, DFunLike.coe, PowerSeries.coeff_X_pow_mul
-- 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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
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 *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)
i : ℕ
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((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)
        ((↑⋯.unit⁻¹ : A⟦X⟧) *
          ((↑r : A⟦X⟧) -
            (↑((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_of_coeff_right_mem_ideal' (fun i ↦ ?_) _

Premises used: PowerSeries.coeff_mul_mem_ideal_of_coeff_right_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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
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 *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)
i : ℕ
succ :
  ∀ (i : ℕ),
    Membership.mem (α := A) (I ^ (k + 1))
      ((coeff i : (a : A⟦X⟧) → A)
          ((↑r : A⟦X⟧) -
            (↑((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 + (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
          (a : A⟦X⟧) → A)
        ((↑⋯.unit⁻¹ : A⟦X⟧) *
          ((↑r : A⟦X⟧) -
            (↑((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_of_coeff_right_mem_ideal' (fun i ↦ ?_) _

Premises used: PowerSeries.coeff_mul_mem_ideal_of_coeff_right_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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
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 *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)
i_1 i : ℕ
succ :
  HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : 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])
                  g) :
              A⟦X⟧) *
            q) :
        A) ∈
    I ^ (k + 1)
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        ((↑r : A⟦X⟧) -
          (↑((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:
rw [map_sub]

Premises used: map_sub
-- 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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
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 *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)
i_1 i : ℕ
⊢ HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : 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])
                  g) :
              A⟦X⟧) *
            q) :
        A) ∈
    I ^ (k + 1)

Tactic:
Ideal.sub_mem _ (h1 _) ?_

Premises used: Set.Mem, Ideal.sub_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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
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 *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((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)
i_1 i : ℕ
succ :
  Membership.mem (α := A) (I ^ (k + 1))
    ((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])
                g) :
            A⟦X⟧) *
          q) :
      A)
⊢ HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : 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])
                  g) :
              A⟦X⟧) *
            q) :
        A) ∈
    I ^ (k + 1)

Tactic:
refine Ideal.sub_mem _ (h1 _) ?_

Premises used: Ideal.sub_mem