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
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 : ℕ
⊢ ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
have zero : ∀ (i : ℕ), Membership.mem (α := A) (HPow.hPow (β := ℕ) I 0) ((coeff i : (a : A⟦X⟧) → A) q : A)
Tactic: induction k with
  | zero => simp
  | succ k ih =>
    rw [g.eq_X_pow_mul_shift_add_trunc (g.map (Ideal.Quotient.mk I)).order.toNat] at heq
    have h1 : ∀ i, coeff i r ∈ I ^ (k + 1) := fun i ↦ by
      rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi
      · rw [← heq, pow_succ']
        refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal i (fun j hj ↦ ?_)
          (fun j _ ↦ ih j) i le_rfl
        rw [map_add, Polynomial.coeff_coe]
        refine Ideal.add_mem _ ?_ (g.coeff_trunc_order_mem I j)
        simp_rw [coeff_X_pow_mul', if_neg (lt_of_le_of_lt hj hi).not_ge, zero_mem]
      simp_rw [Polynomial.coeff_coe,
        Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg (by simpa)), zero_mem]
    rw [add_mul, mul_comm (X ^ _), ← eq_sub_iff_add_eq] at heq
    replace heq := congr(H.isUnit_shift.unit⁻¹ * $heq)
    rw [← mul_assoc, ← mul_assoc, IsUnit.val_inv_mul, one_mul] at heq
    intro i
    rw [← coeff_X_pow_mul _ (g.map (Ideal.Quotient.mk I)).order.toNat i, heq]
    refine coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (fun i ↦ ?_) _
    rw [map_sub]
    refine Ideal.sub_mem _ (h1 _) ?_
    rw [pow_succ']
    refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (fun i ↦ ?_) ih _
    simp_rw [Polynomial.coeff_coe, g.coeff_trunc_order_mem]
Cleared hypotheses: 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⟧)
k : ℕ
zero : ∀ (i : ℕ), Membership.mem (α := A) (HPow.hPow (β := ℕ) I 0) ((coeff i : (a : A⟦X⟧) → A) q : A)
⊢ ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
have succ : ∀ (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: induction k with
  | zero => simp
  | succ k ih =>
    rw [g.eq_X_pow_mul_shift_add_trunc (g.map (Ideal.Quotient.mk I)).order.toNat] at heq
    have h1 : ∀ i, coeff i r ∈ I ^ (k + 1) := fun i ↦ by
      rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi
      · rw [← heq, pow_succ']
        refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal i (fun j hj ↦ ?_)
          (fun j _ ↦ ih j) i le_rfl
        rw [map_add, Polynomial.coeff_coe]
        refine Ideal.add_mem _ ?_ (g.coeff_trunc_order_mem I j)
        simp_rw [coeff_X_pow_mul', if_neg (lt_of_le_of_lt hj hi).not_ge, zero_mem]
      simp_rw [Polynomial.coeff_coe,
        Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg (by simpa)), zero_mem]
    rw [add_mul, mul_comm (X ^ _), ← eq_sub_iff_add_eq] at heq
    replace heq := congr(H.isUnit_shift.unit⁻¹ * $heq)
    rw [← mul_assoc, ← mul_assoc, IsUnit.val_inv_mul, one_mul] at heq
    intro i
    rw [← coeff_X_pow_mul _ (g.map (Ideal.Quotient.mk I)).order.toNat i, heq]
    refine coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (fun i ↦ ?_) _
    rw [map_sub]
    refine Ideal.sub_mem _ (h1 _) ?_
    rw [pow_succ']
    refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (fun i ↦ ?_) ih _
    simp_rw [Polynomial.coeff_coe, g.coeff_trunc_order_mem]
Cleared hypotheses: k
-- 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 q' : A⟦X⟧
r r' : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hr' :
  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⟧) = g * q' + (↑r' : A⟦X⟧)
⊢ g * (q - q') = (↑(r' - r) : A⟦X⟧)
have heq₁ : g * q = g * q' + (↑r' : A⟦X⟧) - (↑r : A⟦X⟧)
Tactic: rw [← eq_sub_iff_add_eq] at heq
Cleared hypotheses: 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 q' : A⟦X⟧
r r' : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hr' :
  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 = g * q' + (↑r' : A⟦X⟧) - (↑r : A⟦X⟧)
⊢ g * (q - q') = (↑(r' - r) : A⟦X⟧)
have rw : g * q' + (↑r' : A⟦X⟧) - (↑r : A⟦X⟧) - g * q' = (↑r' : A⟦X⟧) - (↑r : A⟦X⟧)
Tactic: rw [Polynomial.coe_sub, mul_sub, heq]
-- 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 q' : A⟦X⟧
r r' : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hr' :
  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⟧) = g * q' + (↑r' : A⟦X⟧)
⊢ q = q' ∧ r = r'
have heq₁ : g * (q - q') = (↑(r' - r) : A⟦X⟧)
Tactic: replace heq : g * (q - q') = ↑(r' - r) := by
    rw [← eq_sub_iff_add_eq] at heq
    rw [Polynomial.coe_sub, mul_sub, heq]
    ring
Cleared hypotheses: heq
-- 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 q' : A⟦X⟧
r r' : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hr' :
  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 - q') = (↑(r' - r) : A⟦X⟧)
⊢ q = q' ∧ r = r'
have h : q - q' = 0 ∧ r' - r = 0
Tactic: have h := H.eq_zero_of_mul_eq (lt_of_le_of_lt (r'.degree_sub_le r) (max_lt hr' hr)) heq
-- 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 q' : A⟦X⟧
r r' : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hr' :
  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 - q') = (↑(r' - r) : A⟦X⟧)
h : q - q' = 0 ∧ r' - r = 0
⊢ q = q' ∧ r = r'
have h₁ : q = q' ∧ r' = r
Tactic: simp_rw [sub_eq_zero] at h
Cleared hypotheses: h
-- 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 f' : A⟦X⟧
inst_1 : IsAdicComplete I A
⊢ H.div (f + f') = H.div f + H.div f'
have H1 : (f + f').IsWeierstrassDivisionAt g (H.div f + H.div f') (H.mod f + H.mod f') I
Tactic: have H1 := (H.isWeierstrassDivisionAt_div_mod f).add (H.isWeierstrassDivisionAt_div_mod f')
-- 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 f' : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (f + f').IsWeierstrassDivisionAt g (H.div f + H.div f') (H.mod f + H.mod f') I
⊢ H.div (f + f') = H.div f + H.div f'
have H2 : (f + f').IsWeierstrassDivisionAt g (H.div (f + f')) (H.mod (f + f')) I
Tactic: have H2 := H.isWeierstrassDivisionAt_div_mod (f + f')
-- 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
a : A
f : A⟦X⟧
inst_1 : IsAdicComplete I A
⊢ H.div (a • f) = a • H.div f
have H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
Tactic: have H1 := (H.isWeierstrassDivisionAt_div_mod f).smul a
-- 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
a : A
f : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
⊢ H.div (a • f) = a • H.div f
have H2 : (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I
Tactic: have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)
-- 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 f' : A⟦X⟧
inst_1 : IsAdicComplete I A
⊢ H.mod (f + f') = H.mod f + H.mod f'
have H1 : (f + f').IsWeierstrassDivisionAt g (H.div f + H.div f') (H.mod f + H.mod f') I
Tactic: have H1 := (H.isWeierstrassDivisionAt_div_mod f).add (H.isWeierstrassDivisionAt_div_mod f')
-- 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 f' : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (f + f').IsWeierstrassDivisionAt g (H.div f + H.div f') (H.mod f + H.mod f') I
⊢ H.mod (f + f') = H.mod f + H.mod f'
have H2 : (f + f').IsWeierstrassDivisionAt g (H.div (f + f')) (H.mod (f + f')) I
Tactic: have H2 := H.isWeierstrassDivisionAt_div_mod (f + f')
-- 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
a : A
f : A⟦X⟧
inst_1 : IsAdicComplete I A
⊢ H.mod (a • f) = a • H.mod f
have H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
Tactic: have H1 := (H.isWeierstrassDivisionAt_div_mod f).smul a
-- 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
a : A
f : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
⊢ H.mod (a • f) = a • H.mod f
have H2 : (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I
Tactic: have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)
-- 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
a : A
f_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
⊢ Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
have hf₁ : Membership.mem (γ := Submodule A⟦X⟧ A⟦X⟧) (Ideal.span {g}) (f - f')
Tactic: have hf := (Submodule.quotientRel_def (p := Ideal.span {g})).mp hf
-- 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
a : A
f_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : A⟦X⟧
hf_1 : f ≈ f'
hf : Membership.mem (γ := Submodule A⟦X⟧ A⟦X⟧) (Ideal.span {g}) (f - f')
⊢ Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
have hf₁ : ∃ (a : A⟦X⟧), a * g = f - f'
Tactic: rw [Ideal.mem_span_singleton'] at hf
Cleared hypotheses: hf
-- 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_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : A⟦X⟧
hf_1 : f ≈ f'
hf : ∃ (a : A⟦X⟧), a * g = f - f'
⊢ Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
have obtain : ∀ (a : A⟦X⟧) (ha : a * g = f - f'),
  Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
Tactic: obtain ⟨a, ha⟩ := hf
Cleared hypotheses: hf
-- 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
a_1 : A
f_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
⊢ Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
have hf1 : (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: obtain ⟨hf1, hf2⟩ := H.isWeierstrassDivisionAt_div_mod f
-- 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
a_1 : A
f_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
hf1 :
  (H.mod f).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
⊢ Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
have hf2 : f = g * H.div f + (↑(H.mod f) : A⟦X⟧)
Tactic: obtain ⟨hf1, hf2⟩ := H.isWeierstrassDivisionAt_div_mod f
-- 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
a_1 : A
f_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
hf1 :
  (H.mod f).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hf2 : f = g * H.div f + (↑(H.mod f) : A⟦X⟧)
⊢ Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
have hf'1 : (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: obtain ⟨hf'1, hf'2⟩ := H.isWeierstrassDivisionAt_div_mod f'
-- 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
a_1 : A
f_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
hf1 :
  (H.mod f).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hf2 : f = g * H.div f + (↑(H.mod f) : A⟦X⟧)
hf'1 :
  (H.mod f').degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
⊢ Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
have hf'2 : f' = g * H.div f' + (↑(H.mod f') : A⟦X⟧)
Tactic: obtain ⟨hf'1, hf'2⟩ := H.isWeierstrassDivisionAt_div_mod f'
-- 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
a_1 : A
f_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g = f - f'
hf1 :
  (H.mod f).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hf2 : f = g * H.div f + (↑(H.mod f) : A⟦X⟧)
hf'1 :
  (H.mod f').degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
hf'2 : f' = g * H.div f' + (↑(H.mod f') : A⟦X⟧)
⊢ Eq.{u_1 + 1} (α := A[X]) ((fun (f : A⟦X⟧) ↦ H.mod f) f) ((fun (f : A⟦X⟧) ↦ H.mod f) f')
have ha₁ : g * (a + H.div f') + (↑(H.mod f') : A⟦X⟧) = g * H.div f + (↑(H.mod f) : A⟦X⟧)
Tactic: rw [eq_sub_iff_add_eq, hf2, hf'2, ← add_assoc, mul_comm, ← mul_add] at ha
Cleared hypotheses: ha, hf1, hf2, hf'1, hf'2
-- 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_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f f' : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})
⊢ Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯ (f + f') =
    HAdd.hAdd (α := A[X]) (Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯ f) (Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯ f')
have obtain : ∀ (f : A⟦X⟧),
  Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) sorry
      (HAdd.hAdd (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f :
          HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
        f') =
    HAdd.hAdd (α := A[X])
      (Quotient.lift (s := Submodule.quotientRel (R := A⟦X⟧) (Ideal.span {g})) (fun (f : A⟦X⟧) ↦ H.mod f) sorry
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f))
      (Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) sorry f')
Tactic: obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
Cleared hypotheses: f
-- 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_1 f'_1 : A⟦X⟧
inst_1 : IsAdicComplete I A
f' : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})
f : A⟦X⟧
⊢ Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯
      (HAdd.hAdd (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f :
          HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
        f') =
    HAdd.hAdd (α := A[X])
      (Quotient.lift (s := Submodule.quotientRel (R := A⟦X⟧) (Ideal.span {g})) (fun (f : A⟦X⟧) ↦ H.mod f) ⋯
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f))
      (Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯ f')
have obtain : ∀ (f' : A⟦X⟧),
  Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) sorry
      (HAdd.hAdd (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})) (β :=
        HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f :
          HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f' :
          HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))) =
    HAdd.hAdd (α := A[X])
      (Quotient.lift (s := Submodule.quotientRel (R := A⟦X⟧) (Ideal.span {g})) (fun (f : A⟦X⟧) ↦ H.mod f) sorry
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f))
      (Quotient.lift (s := Submodule.quotientRel (R := A⟦X⟧) (Ideal.span {g})) (fun (f : A⟦X⟧) ↦ H.mod f) sorry
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f'))
Tactic: obtain ⟨f', rfl⟩ := Ideal.Quotient.mk_surjective f'
Cleared hypotheses: f'
-- 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_1 : A
f_1 f' : A⟦X⟧
inst_1 : IsAdicComplete I A
a : A
f : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})
⊢ Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯ (a • f) =
    HSMul.hSMul (α := A) (β := A[X]) ((RingHom.id A : (a : A) → A) a : A) (Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯ f)
have obtain : ∀ (f : A⟦X⟧),
  Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) sorry
      (HSMul.hSMul (β := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})) a
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f :
          HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))) =
    HSMul.hSMul (α := A) (β := A[X]) ((RingHom.id A : (a : A) → A) a : A)
      (Quotient.lift (s := Submodule.quotientRel (R := A⟦X⟧) (Ideal.span {g})) (fun (f : A⟦X⟧) ↦ H.mod f) sorry
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f))
Tactic: obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
Cleared hypotheses: f
-- 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 : IsAdicComplete I A
r : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
⊢ H.div (↑r : A⟦X⟧) = 0
have h1 : (H.mod (↑r : A⟦X⟧)).degree <
  (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
Tactic: obtain ⟨h1, h2⟩ := H.isWeierstrassDivisionAt_div_mod r
-- 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 : IsAdicComplete I A
r : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
h1 :
  (H.mod (↑r : A⟦X⟧)).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
⊢ H.div (↑r : A⟦X⟧) = 0
have h2 : (↑r : A⟦X⟧) = g * H.div (↑r : A⟦X⟧) + (↑(H.mod (↑r : A⟦X⟧)) : A⟦X⟧)
Tactic: obtain ⟨h1, h2⟩ := H.isWeierstrassDivisionAt_div_mod r
-- 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 : IsAdicComplete I A
r : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
⊢ H.mod (↑r : A⟦X⟧) = r
have h1 : (H.mod (↑r : A⟦X⟧)).degree <
  (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
Tactic: obtain ⟨h1, h2⟩ := H.isWeierstrassDivisionAt_div_mod r
-- 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 : IsAdicComplete I A
r : A[X]
hr :
  r.degree < (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
h1 :
  (H.mod (↑r : A⟦X⟧)).degree <
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ)
⊢ H.mod (↑r : A⟦X⟧) = r
have h2 : (↑r : A⟦X⟧) = g * H.div (↑r : A⟦X⟧) + (↑(H.mod (↑r : A⟦X⟧)) : A⟦X⟧)
Tactic: obtain ⟨h1, h2⟩ := H.isWeierstrassDivisionAt_div_mod r
-- 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 : IsAdicComplete I A
f : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})
⊢ (Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g})
      (↑((H.mod' : (a : A⟦X⟧ ⧸ Ideal.span {g}) → A[X]) f) : A⟦X⟧) =
    f
have obtain : ∀ (f : A⟦X⟧),
  Eq (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
    ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g})
        (↑((H.mod' : (a : A⟦X⟧ ⧸ Ideal.span {g}) → A[X])
              ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f)) :
          A⟦X⟧) :
      HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
    ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f :
      HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g}))
Tactic: obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
Cleared hypotheses: f