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 : IsAdicComplete I A
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}))
have rw : ∃ (a : A⟦X⟧), a * g = f - (↑(H.mod f) : A⟦X⟧)
Tactic: rw [mod'_mk_eq_mod, Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']
-- 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 : A⟦X⟧
⊢ ∃ (a : A⟦X⟧), a * g = f - (↑(H.mod f) : A⟦X⟧)
have h : H.div f * g = f - (↑(H.mod f) : A⟦X⟧)
Tactic: use H.div 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
inst_1 : IsAdicComplete I A
f : A⟦X⟧
⊢ H.div f * g = f - (↑(H.mod f) : A⟦X⟧)
have h : H.div f * g + (↑(H.mod f) : A⟦X⟧) = f
Tactic: rw [eq_sub_iff_add_eq, mul_comm, (H.isWeierstrassDivisionAt_div_mod f).2.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
inst_1 : IsAdicComplete I A
f : A⟦X⟧
h : H.div f * g + (↑(H.mod f) : A⟦X⟧) = f
⊢ H.div f * g = f - (↑(H.mod f) : A⟦X⟧)
have h₁ : g * H.div f + (↑(H.mod f) : A⟦X⟧) = f
Tactic: rw [eq_sub_iff_add_eq, mul_comm, (H.isWeierstrassDivisionAt_div_mod f).2.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
inst_1 : IsAdicComplete I A
f : A⟦X⟧
h : H.div f * g + (↑(H.mod f) : A⟦X⟧) = f
h₁ : g * H.div f + (↑(H.mod f) : A⟦X⟧) = f
⊢ H.div f * g = f - (↑(H.mod f) : A⟦X⟧)
have h₂ : f = f
Tactic: rw [eq_sub_iff_add_eq, mul_comm, (H.isWeierstrassDivisionAt_div_mod f).2.symm]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
a : A[X]
ha : Membership.mem (γ := Submodule A[X] A[X]) (Ideal.span {g}) a
⊢ Membership.mem (γ := Submodule A[X] A[X])
    (Ideal.comap (F := A[X] →ₐ[A] A⟦X⟧) (Polynomial.coeToPowerSeries.algHom A) (Ideal.span {(↑g : A⟦X⟧)})) a
have obtain : ∀ (b : A[X]) (hb : b * g = a),
  Membership.mem (γ := Submodule A[X] A[X])
    (Ideal.comap (F := A[X] →ₐ[A] A⟦X⟧) (Polynomial.coeToPowerSeries.algHom A) (Ideal.span {(↑g : A⟦X⟧)})) a
Tactic: obtain ⟨b, hb⟩ := Ideal.mem_span_singleton'.1 ha
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
a : A[X]
ha : Membership.mem (γ := Submodule A[X] A[X]) (Ideal.span {g}) a
b : A[X]
hb : b * g = a
⊢ Membership.mem (γ := Submodule A[X] A[X])
    (Ideal.comap (F := A[X] →ₐ[A] A⟦X⟧) (Polynomial.coeToPowerSeries.algHom A) (Ideal.span {(↑g : A⟦X⟧)})) a
have simp : ∃ (a_1 : A⟦X⟧), a_1 * (↑g : A⟦X⟧) = (↑a : A⟦X⟧)
Tactic: simp only [Ideal.mem_comap, Polynomial.coeToPowerSeries.algHom_apply, Algebra.algebraMap_self,
      map_id, id_eq, Ideal.mem_span_singleton']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
⊢ Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
have inl : Subsingleton A →
  Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑sorry.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) sorry)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
Tactic: rcases subsingleton_or_nontrivial A with _ | _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
inl :
  Subsingleton A →
    Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
        (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
        (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
        (OneHom.toFun
          (↑(↑(AlgHom.toRingHom (R := A)
                    (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
                A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
            OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
          f) =
      f
⊢ Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
have inr : Nontrivial A →
  Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑sorry.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) sorry)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
Tactic: rcases subsingleton_or_nontrivial A with _ | _
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
h : Subsingleton A
⊢ Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
have this : Subsingleton.{u_1 + 1} A[X]
Tactic: have : Subsingleton A[X] := inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
h : Subsingleton A
this : Subsingleton.{u_1 + 1} A[X]
⊢ Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
have this₁ : Subsingleton.{u_1 + 1} (HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g}))
Tactic: have : Subsingleton (A[X] ⧸ Ideal.span {g}) := Quot.Subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
h : Nontrivial A
⊢ Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
have hI : I ≠ ⊤
Tactic: have hI : I ≠ ⊤ := by
      rintro rfl
      exact not_subsingleton _ ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
h : Nontrivial A
hI : I ≠ ⊤
⊢ Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
have this : Nontrivial.{u_1} (A ⧸ I)
Tactic: have := Ideal.Quotient.nontrivial_iff.mpr hI
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
⊢ ∃ (r : A[X]), r.degree < g.degree ∧ (Ideal.Quotient.mk (Ideal.span {g}) : (a : A[X]) → A[X] ⧸ Ideal.span {g}) r = f
have obtain : ∀ (f : A[X]),
  ∃ (r : A[X]),
    r.degree < g.degree ∧
      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}) r :
          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
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
f : A[X]
⊢ ∃ (r : A[X]),
    r.degree < g.degree ∧
      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}) r :
          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}))
have refine : 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}) (f %ₘ 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}))
Tactic: refine ⟨f %ₘ g, Polynomial.degree_modByMonic_lt f H.monic, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
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}) (f %ₘ 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}))
have rw : ∃ (a : A[X]), a * g = f - f %ₘ g
Tactic: rw [Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
f : A[X]
⊢ f /ₘ g * g = f - f %ₘ g
have rw : f /ₘ g * g = f - (f - g * (f /ₘ g))
Tactic: rw [Polynomial.modByMonic_eq_sub_mul_div]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
⊢ Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
      (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
      (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
      (OneHom.toFun
        (↑(↑(AlgHom.toRingHom (R := A)
                  (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
              A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
          OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
        f) =
    f
have inr : ∀ (f : A[X]) (hfdeg : f.degree < g.degree),
  Eq (α := HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g}))
    (Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
        (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
        (⇑sorry.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
        (OneHom.toFun (M := HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g}))
          (↑(↑(AlgHom.toRingHom (R := A)
                    (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) sorry)) :
                A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
            OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
          ((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}))
Tactic: obtain ⟨f, hfdeg, rfl⟩ : ∃ r : A[X], r.degree < g.degree ∧ Ideal.Quotient.mk _ r = f := by
      obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
      refine ⟨f %ₘ g, Polynomial.degree_modByMonic_lt f H.monic, ?_⟩
      rw [Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']
      exact ⟨f /ₘ g, by rw [Polynomial.modByMonic_eq_sub_mul_div]; ring⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
⊢ ((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 (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
⊢ g.degree =
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧))).toNat : WithBot ℕ)
have h : (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧))).toNat =
  (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧))).lift sorry
Tactic: convert!
        H.degree_eq_coe_lift_order_map g 1 (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one])
          (by simp)
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
⊢ Eq (α := HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g}))
    (Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
        (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
        (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
        (OneHom.toFun (M := HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g}))
          (↑(↑(AlgHom.toRingHom (R := A)
                    (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
                A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
            OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
          ((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}))
have h1 : g.degree =
  (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧))).toNat : WithBot ℕ)
Tactic: have h1 : g.degree = ((g : A⟦X⟧).map (Ideal.Quotient.mk I)).order.toNat := by
      convert!
        H.degree_eq_coe_lift_order_map g 1 (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one])
          (by simp)
      exact (ENat.lift_eq_toNat_of_lt_top _).symm
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
h1 :
  g.degree =
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧))).toNat : WithBot ℕ)
⊢ Eq (α := HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g}))
    (Function.comp (α := HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : A⟦X⟧)})) (β := A[X])
        (⇑(Ideal.Quotient.mk (Ideal.span {g})) : (a : A[X]) → A[X] ⧸ Ideal.span {g})
        (⇑⋯.mod' : (a : A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) → A[X])
        (OneHom.toFun (M := HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g}))
          (↑(↑(AlgHom.toRingHom (R := A)
                    (Ideal.quotientMapₐ (Ideal.span {(↑g : A⟦X⟧)}) (Polynomial.coeToPowerSeries.algHom A) ⋯)) :
                A[X] ⧸ Ideal.span {g} →* A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}) :
            OneHom (A[X] ⧸ Ideal.span {g}) (A⟦X⟧ ⧸ Ideal.span {(↑g : A⟦X⟧)}))
          ((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}))
have inr : 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}) (sorry.mod (↑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: dsimp
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I_1 : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst_1 : IsAdicComplete I A
h : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
h1 :
  g.degree =
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) (↑g : A⟦X⟧))).toNat : WithBot ℕ)
⊢ 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}) (⋯.mod (↑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}))
have inr : ∃ (a : A[X]), a * g = sorry.mod (↑f : A⟦X⟧) - f
Tactic: rw [Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ f /ʷ 0 = 0
have rw : Eq.{u_1 + 1} (α := A⟦X⟧)
  (if hg :
      Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) 0 :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
    IsWeierstrassDivisorAt.div sorry f
  else 0)
  0
Tactic: rw [weierstrassDiv, dif_neg (by simp)]