awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 ≠ ⊤
⊢ 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⟧)
have 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)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: rw [Polynomial.coeff_coe, coeff_trunc]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 : ℕ
⊢ 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)
have 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)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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)
⊢ 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)
have 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)
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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)
have 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)
Tactic: refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 : ℕ
⊢ 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)
have 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
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]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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
have h : ∀ (i : ℕ), Eq (α := A) ((coeff i : (a : A⟦X⟧) → A) q : A) ((coeff i : (a : A⟦X⟧) → A) 0 : A)
Tactic: ext i
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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)
have h : ∀ (k : ℕ),
  SModEq (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ k) ⊤) ((coeff i : (a : A⟦X⟧) → A) q : A) (0 : A)
Tactic: refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 : ℕ
⊢ SModEq (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ k) ⊤) ((coeff i : (a : A⟦X⟧) → A) q : A) (0 : A)
have h : Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
Tactic: rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
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 ∧ r = 0
have hq : 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 _ _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
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
⊢ q = 0 ∧ r = 0
have heq₁ : r = 0
Tactic: rw [hq, mul_zero, Eq.comm, Polynomial.coe_eq_zero_iff] at heq
Cleared hypotheses: heq, this, hq
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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⟧)
⊢ q = 0 ∧ r = 0
have suffices : ∀ (k i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
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⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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)
⊢ ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) q : A)
have 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)
Tactic: rw [g.eq_X_pow_mul_shift_add_trunc (g.map (Ideal.Quotient.mk I)).order.toNat] at heq
Cleared hypotheses: heq, k, ih
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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)
have 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)
Tactic: rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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)
⊢ Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
have 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)
Tactic: rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
have 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)
Tactic: rw [← heq, pow_succ']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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)
have 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)
Tactic: refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal i (fun j hj ↦ ?_)
          (fun j _ ↦ ih j) i le_rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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
⊢ 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)
have 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
Tactic: rw [map_add, Polynomial.coeff_coe]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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
have 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)
Tactic: refine Ideal.add_mem _ ?_ (g.coeff_trunc_order_mem I j)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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
⊢ 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)
have 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)
Tactic: simp_rw [coeff_X_pow_mul', if_neg (lt_of_le_of_lt hj hi).not_ge, zero_mem]