awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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⟧)
⊢ Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (f - g * q') : A)
have key : f - g * q' = (↑s₀ : A⟦X⟧) - (↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑sorry.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
-- 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⟧)
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 ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (f - g * q') : A)
have succ : Membership.mem (α := A) (I * I ^ k)
  ((coeff i : (a : A⟦X⟧) → A) ((↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁ * (↑sorry.unit⁻¹ : A⟦X⟧)) : A)
Tactic: rw [key, map_sub, Polynomial.coeff_coe, coeff_trunc, if_neg hi.not_gt, zero_sub, neg_mem_iff,
      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
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)
have 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)
Tactic: refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) 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⟧
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 : ℕ
⊢ Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A) ((↑((trunc n : (a : A⟦X⟧) → A[X]) g) : A⟦X⟧) * s₁) : A)
have succ : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) 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
-- 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_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 : (a : A⟦X⟧) → A) s₁ : A)
have succ : Membership.mem (α := A) (I ^ k) ((coeff (i + n) : (a : A⟦X⟧) → A) s : A)
Tactic: rw [coeff_mk]
-- 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
⊢ Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
have 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)
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)
Cleared hypotheses: k, i, 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⟧
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)
⊢ Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (f - g * H.seq f k) : A)
have 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)
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)
Cleared hypotheses: k, i, 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⟧
k i : ℕ
⊢ Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) (H.seq f (k + 1) - H.seq f k) : A)
have rw : Membership.mem (α := A) (I ^ k)
  ((coeff i : (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)
            (f - g * H.seq f k)) *
        (↑sorry.unit⁻¹ : A⟦X⟧)) :
    A)
Tactic: rw [seq, add_sub_cancel_left]
-- 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 : ℕ
⊢ Membership.mem (α := A) (I ^ k)
    ((coeff i : (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)
              (f - g * H.seq f k)) *
          (↑⋯.unit⁻¹ : A⟦X⟧)) :
      A)
have refine : ∀ (i : ℕ),
  Membership.mem (α := A) (I ^ k)
    ((coeff i : (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)
            (f - g * H.seq f k)) :
      A)
Tactic: refine coeff_mul_mem_ideal_of_coeff_left_mem_ideal' (fun i ↦ ?_) 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⟧
k i_1 i : ℕ
⊢ Membership.mem (α := A) (I ^ k)
    ((coeff i : (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)
            (f - g * H.seq f k)) :
      A)
have rw : Membership.mem (α := A) (I ^ k)
  ((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) :
    A)
Tactic: rw [coeff_mk]
-- 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⟧
⊢ H.seq f 1 =
    (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) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
have simp_rw : 0 +
    (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 * 0)) *
      (↑sorry.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)
        f) *
    (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: simp_rw [seq, mul_zero, zero_add, sub_zero]
-- 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⟧
simp_rw :
  0 +
      (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 * 0)) *
        (↑⋯.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)
          f) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ H.seq f 1 =
    (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) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
have simp_rw₁ : 0 +
    (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 - 0)) *
      (↑sorry.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)
        f) *
    (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: simp_rw [seq, mul_zero, zero_add, sub_zero]
-- 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⟧
simp_rw :
  0 +
      (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 * 0)) *
        (↑⋯.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)
          f) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
simp_rw₁ :
  0 +
      (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 - 0)) *
        (↑⋯.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)
          f) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
⊢ H.seq f 1 =
    (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) *
      (↑⋯.unit⁻¹ : A⟦X⟧)
have simp_rw₂ : (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 - 0)) *
    (↑sorry.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)
        f) *
    (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: simp_rw [seq, mul_zero, zero_add, sub_zero]
-- 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
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n : ℕ
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
have base : Eq.{u_1 + 1} (α := A ⧸ HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
  (Submodule.Quotient.mk ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m))
  (Submodule.Quotient.mk ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m))
Tactic: rw [SModEq.def]
-- 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
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n_1 n : ℕ
hn : m ≤ n
ih :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))
have succ : SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
  ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))
  ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
Tactic: refine ih.trans (SModEq.symm ?_)
-- 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
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n_1 n : ℕ
hn : m ≤ n
ih :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
have succ : Membership.mem (α := A) (I ^ m) ((coeff i : (a : A⟦X⟧) → A) (H.seq f (n + 1) - H.seq f n) : A)
Tactic: rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← 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
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n : ℕ
hn : m ≤ n
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
have base : SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
  ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
  ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
Tactic: induction n, hn using Nat.le_induction with
      | base => rw [SModEq.def]
      | succ n hn ih =>
        refine ih.trans (SModEq.symm ?_)
        rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← map_sub]
        exact Ideal.pow_le_pow_right hn (H.coeff_seq_succ_sub_seq_mem f n i)
Cleared hypotheses: hn
-- 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
a : A
f f' : A⟦X⟧
inst_1 : IsPrecomplete I A
i m n : ℕ
hn : m ≤ n
base :
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
⊢ SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)
have succ : ∀ (n : ℕ) (hn : m ≤ n)
  (ih :
    SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
      ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
      ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) n)),
  SModEq.{u_1, u_1} (R := A) (M := A) (HSMul.hSMul (β := Submodule A A) (I ^ m) ⊤)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) m)
    ((fun (k : ℕ) ↦ ((coeff i : (a : A⟦X⟧) → A) (H.seq f k) : A)) (n + 1))
Tactic: induction n, hn using Nat.le_induction with
      | base => rw [SModEq.def]
      | succ n hn ih =>
        refine ih.trans (SModEq.symm ?_)
        rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← map_sub]
        exact Ideal.pow_le_pow_right hn (H.coeff_seq_succ_sub_seq_mem f n i)
Cleared hypotheses: hn
-- 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
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I
have inl : ∀ (H : g.IsWeierstrassDivisorAt ⊤) [inst_2 : IsAdicComplete (R := A) ⊤ A],
  f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) ⊤
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.IsWeierstrassDivisorAt I
f : A⟦X⟧
inst_1 : IsAdicComplete I A
inl :
  ∀ (H : g.IsWeierstrassDivisorAt ⊤) [inst_2 : IsAdicComplete (R := A) ⊤ A],
    f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) ⊤
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I
have inr : ∀ (hI : I ≠ ⊤), f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) 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 f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst_1 : IsAdicComplete (R := A) ⊤ A
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) ⊤
have this : Subsingleton A
Tactic: have := ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g f : A⟦X⟧
H : g.IsWeierstrassDivisorAt ⊤
inst_1 : IsAdicComplete (R := A) ⊤ A
this : Subsingleton A
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) ⊤
have inl : IsWeierstrassDivisionAt 0 g 0 0 ⊤
Tactic: rw [Subsingleton.elim f 0, Subsingleton.elim (H.div 0) 0, Subsingleton.elim (H.mod 0) 0]
-- 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.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I
have inr : (H.mod f).degree <
  (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
Tactic: constructor
-- 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 ≠ ⊤
inr :
  (H.mod f).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
⊢ f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I
have inr₁ : f = g * H.div f + (↑(H.mod f) : A⟦X⟧)
Tactic: constructor
-- 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 + (↑(H.mod f) : A⟦X⟧)
have inr : 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⟧)
Tactic: rw [mod, add_comm, ← sub_eq_iff_eq_add]