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⟧
inst_1 : IsLocalRing A
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ g.IsWeierstrassDivisor
have rw : ((coeff
          (order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
              ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) : (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
                g)).toNat :
        (a : A⟦X⟧) → A)
      g :
    A) ∉
  IsLocalRing.maximalIdeal A
Tactic: rw [IsWeierstrassDivisor, IsWeierstrassDivisorAt, ← IsLocalRing.notMem_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
inst_1 : IsLocalRing A
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ ((coeff
            (order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
                ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) :
                    (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
                  g)).toNat :
          (a : A⟦X⟧) → A)
        g :
      A) ∉
    IsLocalRing.maximalIdeal A
have h : Ne (α := IsLocalRing.ResidueField A)
  ((coeff
          (order.{u_1} (R := IsLocalRing.ResidueField A)
              ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
        (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
    IsLocalRing.ResidueField A)
  (0 : IsLocalRing.ResidueField A)
Tactic: have h := coeff_order hg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
inst_1 : IsLocalRing A
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
h :
  Ne (α := IsLocalRing.ResidueField A)
    ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
⊢ ((coeff
            (order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
                ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) :
                    (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
                  g)).toNat :
          (a : A⟦X⟧) → A)
        g :
      A) ∉
    IsLocalRing.maximalIdeal A
have contrapose : ∀
  (h :
    Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
      ((coeff
              (order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
                  ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) :
                      (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
                    g)).toNat :
            (a : A⟦X⟧) → A)
          g :
        A)),
  Eq (α := IsLocalRing.ResidueField A)
    ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
Tactic: contrapose h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
inst_1 : IsLocalRing A
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
h :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff
            (order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
                ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) :
                    (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
                  g)).toNat :
          (a : A⟦X⟧) → A)
        g :
      A)
⊢ Eq (α := IsLocalRing.ResidueField A)
    ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
have rwa : Eq (α := IsLocalRing.ResidueField A)
  ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A)
      ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : A⟦X⟧) → A)
        g) :
    IsLocalRing.ResidueField A)
  (0 : IsLocalRing.ResidueField A)
Tactic: rwa [coeff_map, IsLocalRing.residue_eq_zero_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
inst_1 : IsLocalRing A
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
h :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff
            (order.{u_1} (R := HasQuotient.Quotient A (B := Ideal A) (IsLocalRing.maximalIdeal A : Ideal A))
                ((map (Ideal.Quotient.mk (IsLocalRing.maximalIdeal A)) :
                    (a : A⟦X⟧) → (A ⧸ IsLocalRing.maximalIdeal A)⟦X⟧)
                  g)).toNat :
          (a : A⟦X⟧) → A)
        g :
      A)
rwa :
  Eq (α := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A)
        ((coeff
              (order.{u_1} (R := IsLocalRing.ResidueField A)
                  ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
            (a : A⟦X⟧) → A)
          g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
⊢ Eq (α := IsLocalRing.ResidueField A)
    ((coeff
            (order.{u_1} (R := IsLocalRing.ResidueField A)
                ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
          (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
      IsLocalRing.ResidueField A)
    (0 : IsLocalRing.ResidueField A)
have rwa₁ : Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
  ((coeff
          (order.{u_1} (R := IsLocalRing.ResidueField A)
              ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
        (a : A⟦X⟧) → A)
      g :
    A)
Tactic: rwa [coeff_map, IsLocalRing.residue_eq_zero_iff]
-- 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.IsDistinguishedAt I
hI : I ≠ ⊤
⊢ ((constantCoeff : (a : A⟦X⟧) → A) 1 : A) ∉ I
have rwa : 1 ∉ I
Tactic: rwa [constantCoeff_one, ← Ideal.ne_top_iff_one]
-- 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.IsDistinguishedAt I
hI : I ≠ ⊤
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt I
have this : g.natDegree = ENat.toNat (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧)))
Tactic: have : g.natDegree = _ := congr(ENat.toNat $(H.coe_natDegree_eq_order_map g 1
    (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one]) (by simp)))
-- 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.IsDistinguishedAt I
inst_1 : IsHausdorff I A
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt I
have inl : ∀ (H : g.IsDistinguishedAt ⊤) [IsHausdorff (R := A) ⊤ A], (↑g : A⟦X⟧).IsWeierstrassDivisorAt ⊤
Tactic: rcases eq_or_ne I ⊤ with rfl | hI
Cleared hypotheses: I, H, inst_1
-- 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.IsDistinguishedAt I
inst_1 : IsHausdorff I A
inl : ∀ (H : g.IsDistinguishedAt ⊤) [IsHausdorff (R := A) ⊤ A], (↑g : A⟦X⟧).IsWeierstrassDivisorAt ⊤
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt I
have inr : ∀ (hI : I ≠ ⊤), (↑g : A⟦X⟧).IsWeierstrassDivisorAt I
Tactic: rcases eq_or_ne I ⊤ with rfl | hI
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
g : A[X]
H : g.IsDistinguishedAt ⊤
inst_1 : IsHausdorff (R := A) ⊤ A
⊢ (↑g : A⟦X⟧).IsWeierstrassDivisorAt ⊤
have this : Subsingleton A
Tactic: have := ‹IsHausdorff ⊤ A›.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
⊢ Polynomial.coeff
      ((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
          (a : A⟦X⟧) → A[X])
        g)
      i ∈
    I
have rw : Membership.mem (α := A) I
  (if i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat then
      (coeff i : (a : A⟦X⟧) → A) g
    else 0 :
    A)
Tactic: rw [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
i : ℕ
⊢ Membership.mem (α := A) I
    (if i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat then
        (coeff i : (a : A⟦X⟧) → A) g
      else 0 :
      A)
have pos : ∀ (h : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
  Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) g : A)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
i : ℕ
pos :
  ∀ (h : i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) g : A)
⊢ Membership.mem (α := A) I
    (if i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat then
        (coeff i : (a : A⟦X⟧) → A) g
      else 0 :
      A)
have neg : ∀ (h : ¬i < (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat), 0 ∈ I
Tactic: split_ifs with h
-- 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⟧
k : ℕ
hq :
  ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f (k + 1)) : A)
have succ : Membership.mem (α := A) (I ^ (k + 1))
  ((coeff i : (a : A⟦X⟧) → A)
      (f -
        g *
          (H.seq f k +
            (mk fun (i : ℕ) ↦
                (coeff
                      (i + (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                    (a : A⟦X⟧) → A)
                  (f - g * H.seq f k)) *
              (↑sorry.unit⁻¹ : A⟦X⟧))) :
    A)
Tactic: rw [seq]
-- 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⟧
k : ℕ
hq :
  ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (H.seq f k +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    (f - g * H.seq f k)) *
                (↑⋯.unit⁻¹ : A⟦X⟧))) :
      A)
have succ : let q := H.seq f k;
∀
  (hq :
    ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
      Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * q) : A)),
  Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (q +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    (f - g * q)) *
                (↑sorry.unit⁻¹ : A⟦X⟧))) :
      A)
Tactic: set q := H.seq f k
Cleared hypotheses: 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
f : A⟦X⟧
k i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
q : A⟦X⟧ := H.seq f k
hq :
  ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
    Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * q) : A)
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (q +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    (f - g * q)) *
                (↑⋯.unit⁻¹ : A⟦X⟧))) :
      A)
have succ : let s := f - g * q;
∀
  (hq :
    ∀ {i : ℕ} (hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat),
      Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)),
  Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (q +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    s) *
                (↑sorry.unit⁻¹ : A⟦X⟧))) :
      A)
Tactic: set s := f - g * q
Cleared hypotheses: hq
-- 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
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
hi : i ≥ n
hq : ∀ {i : ℕ} (hi : i ≥ n), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (q +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    s) *
                (↑⋯.unit⁻¹ : A⟦X⟧))) :
      A)
have hs : s =
  (HPow.hPow (α := A⟦X⟧) X n * mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s) +
    (↑((trunc n : (a : A⟦X⟧) → A[X]) s) : A⟦X⟧)
Tactic: have hs := s.eq_X_pow_mul_shift_add_trunc n
-- 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⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
hi : i ≥ n
hq : ∀ {i : ℕ} (hi : i ≥ n), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)
s₀ : A[X] := (trunc n : (a : A⟦X⟧) → A[X]) s
hs : s = (HPow.hPow (α := A⟦X⟧) X n * mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s) + (↑s₀ : A⟦X⟧)
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        (f -
          g *
            (q +
              (mk fun (i : ℕ) ↦
                  (coeff
                        (i +
                          (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat) :
                      (a : A⟦X⟧) → A)
                    s) *
                (↑⋯.unit⁻¹ : A⟦X⟧))) :
      A)
have succ : let s₁ : A⟦X⟧ := mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s;
∀ (hs : s = HPow.hPow (α := A⟦X⟧) X n * s₁ + (↑s₀ : A⟦X⟧)),
  Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (f - g * (q + s₁ * (↑sorry.unit⁻¹ : A⟦X⟧))) : A)
Tactic: set s₁ := PowerSeries.mk fun i ↦ coeff (i + n) s
Cleared hypotheses: hs
-- 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⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
hi : i ≥ n
hq : ∀ {i : ℕ} (hi : i ≥ n), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)
s₀ : A[X] := (trunc n : (a : A⟦X⟧) → A[X]) s
s₁ : A⟦X⟧ := mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s
hs : s = HPow.hPow (α := A⟦X⟧) X n * s₁ + (↑s₀ : A⟦X⟧)
q' : A⟦X⟧ := q + s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
have trans : f - g * q' = s + g * (q - q')
Tactic: trans s + g * (q - q')
-- 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⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
hi : i ≥ n
hq : ∀ {i : ℕ} (hi : i ≥ n), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)
s₀ : A[X] := (trunc n : (a : A⟦X⟧) → A[X]) s
s₁ : A⟦X⟧ := mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s
hs : s = HPow.hPow (α := A⟦X⟧) X n * s₁ + (↑s₀ : A⟦X⟧)
q' : A⟦X⟧ := q + s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
trans : f - g * q' = s + g * (q - q')
⊢ f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
have trans₁ : s + g * (q - q') = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: trans s + g * (q - q')
-- 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⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
hi : i ≥ n
hq : ∀ {i : ℕ} (hi : i ≥ n), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)
s₀ : A[X] := (trunc n : (a : A⟦X⟧) → A[X]) s
s₁ : A⟦X⟧ := mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s
hs : s = HPow.hPow (α := A⟦X⟧) X n * s₁ + (↑s₀ : A⟦X⟧)
q' : A⟦X⟧ := q + s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ s + g * (q - (q + s₁ * (↑⋯.unit⁻¹ : A⟦X⟧))) =
    (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
have rw : s + -(g * (↑sorry.unit⁻¹ : A⟦X⟧) * s₁) =
  (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: rw [sub_add_cancel_left, mul_neg, ← mul_assoc, mul_right_comm]
-- 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⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
hi : i ≥ n
hq : ∀ {i : ℕ} (hi : i ≥ n), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)
s₀ : A[X] := (trunc n : (a : A⟦X⟧) → A[X]) s
s₁ : A⟦X⟧ := mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s
hs : s = HPow.hPow (α := A⟦X⟧) X n * s₁ + (↑s₀ : A⟦X⟧)
q' : A⟦X⟧ := q + s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ s + -(g * (↑⋯.unit⁻¹ : A⟦X⟧) * s₁) =
    (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
have nth_rw : s +
    -(((HPow.hPow (α := A⟦X⟧) X n * mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) g) +
            (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧)) *
          (↑sorry.unit⁻¹ : A⟦X⟧) *
        s₁) =
  (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]
-- 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⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
hi : i ≥ n
hq : ∀ {i : ℕ} (hi : i ≥ n), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)
s₀ : A[X] := (trunc n : (a : A⟦X⟧) → A[X]) s
s₁ : A⟦X⟧ := mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s
hs : s = HPow.hPow (α := A⟦X⟧) X n * s₁ + (↑s₀ : A⟦X⟧)
q' : A⟦X⟧ := q + s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ s +
      -(((HPow.hPow (α := A⟦X⟧) X n * mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) g) +
              (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧)) *
            (↑⋯.unit⁻¹ : A⟦X⟧) *
          s₁) =
    (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
have rw : HPow.hPow (α := A⟦X⟧) X n * s₁ + (↑s₀ : A⟦X⟧) +
    -((HPow.hPow (α := A⟦X⟧) X n * 1 + (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * (↑sorry.unit⁻¹ : A⟦X⟧)) * s₁) =
  (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: rw [add_mul, mul_assoc, IsUnit.mul_val_inv, hs]