awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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
s : A⟦X⟧ := 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)
hi₁ :
  let n := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat;
  i ≥ n
⊢ let n := (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat;
  ∀ {i : ℕ} (hi : i ≥ n), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s : A)

Tactic:
set n := (g.map (Ideal.Quotient.mk I)).order.toNat

Premises used: Ideal.Quotient.mk, 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
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 =
    (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
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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)
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⟧)
⊢ let s₀ : A[X] := (trunc n : (a : A⟦X⟧) → A[X]) s;
  s = (HPow.hPow (α := A⟦X⟧) X n * mk fun (i : ℕ) ↦ (coeff (i + n) : (a : A⟦X⟧) → A) s) + (↑s₀ : A⟦X⟧)

Tactic:
set s₀ := s.trunc n

Premises used: DFunLike.coe, PowerSeries.trunc
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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⟧)
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₁ * (↑⋯.unit⁻¹ : A⟦X⟧))) : 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)

Tactic:
set s₁ := PowerSeries.mk fun i ↦ coeff (i + n) s

Premises used: PowerSeries.coeff, HAdd.hAdd, PowerSeries.mk, 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
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⟧)
succ :
  let q' := q + s₁ * (↑⋯.unit⁻¹ : A⟦X⟧);
  Membership.mem (α := A) (I ^ (k + 1)) ((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 + s₁ * (↑⋯.unit⁻¹ : A⟦X⟧))) : A)

Tactic:
set q' := q + s₁ * H.isUnit_shift.unit⁻¹

Premises used: PowerSeries.IsWeierstrassDivisorAt.isUnit_shift, IsUnit.unit
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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')
trans₁ : s + g * (q - q') = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
trans s + g * (q - q')

Premises used: HSub.hSub
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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⟧)
simp_rw : f - g * q' = f - g * q + g * (q - q')
⊢ f - g * q' = s + g * (q - q')

Tactic:
simp_rw [s]
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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' = f - g * q + g * (q - q')

Tactic:
ring
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
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⟧)
simp_rw :
  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⟧)
⊢ s + g * (q - q') = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
simp_rw [q']
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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⟧)
rw :
  s + -(g * (↑⋯.unit⁻¹ : A⟦X⟧) * s₁) =
    (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * 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⟧)

Tactic:
rw [sub_add_cancel_left, mul_neg, ← mul_assoc, mul_right_comm]

Premises used: mul_assoc, sub_add_cancel_left, mul_right_comm, mul_neg
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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⟧)
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⟧)) *
            (↑⋯.unit⁻¹ : A⟦X⟧) *
          s₁) =
    (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * 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⟧)

Tactic:
nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]

Premises used: PowerSeries.eq_X_pow_mul_shift_add_trunc
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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⟧)
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⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)) * s₁) =
    (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * 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⟧)

Tactic:
rw [add_mul, mul_assoc, IsUnit.mul_val_inv, hs]

Premises used: add_mul, IsUnit.mul_val_inv, mul_assoc
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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⟧)
⊢ 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⟧) * (↑⋯.unit⁻¹ : A⟦X⟧)) * s₁) =
    (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)

Tactic:
ring
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
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⟧)

Tactic:
have key : f - g * q' = (s₀ : A⟦X⟧) - (g.trunc n : A⟦X⟧) * s₁ * H.isUnit_shift.unit⁻¹ := by
      trans s + g * (q - q')
      · simp_rw [s]; ring
      simp_rw [q']
      rw [sub_add_cancel_left, mul_neg, ← mul_assoc, mul_right_comm]
      nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]
      rw [add_mul, mul_assoc, IsUnit.mul_val_inv, hs]
      ring
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
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⟧)
key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
succ :
  Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A) ((↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)) : A)
⊢ Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (f - g * q') : A)

Tactic:
rw [key, map_sub, Polynomial.coeff_coe, coeff_trunc, if_neg hi.not_gt, zero_sub, neg_mem_iff,
      pow_succ']

Premises used: PowerSeries.coeff_trunc, neg_mem_iff, map_sub, LE.le.not_gt, if_neg, pow_succ', Polynomial.coeff_coe, zero_sub
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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⟧)
key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A) ((↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)) : A)

Tactic:
coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i

Premises used: PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal'
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
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⟧)
key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
succ :
  ∀ (i : ℕ),
    Membership.mem (α := A) (I * I ^ k)
      ((coeff i : (a : A⟦X⟧) → A) ((↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁) : A)
⊢ Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A) ((↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)) : A)

Tactic:
refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i

Premises used: PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal'
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i_1 : ℕ
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_1 ≥ 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⟧)
key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
i : ℕ
⊢ ∀ (i : ℕ), Membership.mem (α := A) I ((coeff i : (a : A⟦X⟧) → A) (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) : A)

Tactic:
simp [n, g.coeff_trunc_order_mem]

Premises used: _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
f : A⟦X⟧
k i_1 : ℕ
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_1 ≥ 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⟧)
key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
i : ℕ
succ : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s₁ : A)
⊢ Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A) ((↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁) : A)

Tactic:
refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
      (by simp [n, g.coeff_trunc_order_mem]) (fun i ↦ ?_) i

Premises used: 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
f : A⟦X⟧
k i_1 : ℕ
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_1 ≥ 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⟧)
key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
i_2 i : ℕ
succ : Membership.mem (α := A) (I ^ k) ((coeff (i + n) : (a : A⟦X⟧) → A) s : A)
⊢ Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) s₁ : A)

Tactic:
rw [coeff_mk]

Premises used: PowerSeries.coeff_mk
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i_1 : ℕ
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_1 ≥ 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⟧)
key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
i_2 i : ℕ
⊢ i + n ≥ n

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i_1 : ℕ
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_1 ≥ 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⟧)
key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑⋯.unit⁻¹ : A⟦X⟧)
i_2 i : ℕ
⊢ Membership.mem (α := A) (I ^ k) ((coeff (i + n) : (a : A⟦X⟧) → A) s : A)

Tactic:
exact hq (by simp)
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
hi : i ≥ (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
zero :
  ∀ {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) (HPow.hPow (β := ℕ) I 0) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f 0) : A)
succ :
  ∀ (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)
⊢ Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)

Tactic:
induction k generalizing hi i with
  | zero => simp
  | succ k hq =>
    rw [seq]
    set q := H.seq f k
    set s := f - g * q
    set n := (g.map (Ideal.Quotient.mk I)).order.toNat
    have hs := s.eq_X_pow_mul_shift_add_trunc n
    set s₀ := s.trunc n
    set s₁ := PowerSeries.mk fun i ↦ coeff (i + n) s
    set q' := q + s₁ * H.isUnit_shift.unit⁻¹
    have key : f - g * q' = (s₀ : A⟦X⟧) - (g.trunc n : A⟦X⟧) * s₁ * H.isUnit_shift.unit⁻¹ := by
      trans s + g * (q - q')
      · simp_rw [s]; ring
      simp_rw [q']
      rw [sub_add_cancel_left, mul_neg, ← mul_assoc, mul_right_comm]
      nth_rw 1 [g.eq_X_pow_mul_shift_add_trunc n]
      rw [add_mul, mul_assoc, IsUnit.mul_val_inv, hs]
      ring
    rw [key, map_sub, Polynomial.coeff_coe, coeff_trunc, if_neg hi.not_gt, zero_sub, neg_mem_iff,
      pow_succ']
    refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) i
    refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
      (by simp [n, g.coeff_trunc_order_mem]) (fun i ↦ ?_) i
    rw [coeff_mk]
    exact hq (by simp)

Premises used: PowerSeries.coeff_trunc, neg_mem_iff, map_sub, Ideal.Quotient.mk, PowerSeries.coeff_mk, PowerSeries.IsWeierstrassDivisorAt.isUnit_shift, PowerSeries.map, PowerSeries.coeff_mul_mem_ideal_of_coeff_left_mem_ideal', LE.le.not_gt, PowerSeries.order, ENat.toNat, IsUnit.unit, PowerSeries.IsWeierstrassDivisorAt.seq, if_neg, DFunLike.coe, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal', pow_succ', Polynomial.coeff_coe, zero_sub