awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
simp : ∃ (a_1 : A⟦X⟧), a_1 * (↑g : A⟦X⟧) = (↑a : A⟦X⟧)
⊢ 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:
simp only [Ideal.mem_comap, Polynomial.coeToPowerSeries.algHom_apply, Algebra.algebraMap_self,
      map_id, id_eq, Ideal.mem_span_singleton']

Premises used: Ideal.mem_span_singleton', Algebra.algebraMap_self, Polynomial.coeToPowerSeries.algHom_apply, Ideal.mem_comap, PowerSeries.map_id, id_eq
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
⊢ (↑b : A⟦X⟧) * (↑g : A⟦X⟧) = (↑a : A⟦X⟧)

Tactic:
simp [← hb]
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
⊢ ∃ (a_1 : A⟦X⟧), a_1 * (↑g : A⟦X⟧) = (↑a : A⟦X⟧)

Tactic:
exact ⟨b, by simp [← hb]⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
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})
        (⇑⋯.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

Tactic:
rcases subsingleton_or_nontrivial A with _ | _

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
⊢ Subsingleton.{u_1 + 1} A[X]

Tactic:
have : Subsingleton A[X] := inferInstance
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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]
⊢ 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
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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_1 : Subsingleton.{u_1 + 1} A[X]
this : Subsingleton.{u_1 + 1} (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

Tactic:
Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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_1 : Subsingleton.{u_1 + 1} A[X]
this : Subsingleton.{u_1 + 1} (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

Tactic:
exact Subsingleton.elim _ _

Premises used: Subsingleton.elim
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I : Ideal A
g : A[X]
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
h : Nontrivial A
H : g.IsDistinguishedAt ⊤
inst_1 : IsAdicComplete (R := A) ⊤ A
⊢ False

Tactic:
not_subsingleton _ ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton

Premises used: IsAdicComplete.toIsHausdorff, IsHausdorff.subsingleton, not_subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g_1 : A⟦X⟧
I : Ideal A
g : A[X]
f : HasQuotient.Quotient A[X] (B := Ideal A[X]) (Ideal.span {g})
h : Nontrivial A
H : g.IsDistinguishedAt ⊤
inst_1 : IsAdicComplete (R := A) ⊤ A
⊢ False

Tactic:
exact not_subsingleton _ ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton

Premises used: IsAdicComplete.toIsHausdorff, IsHausdorff.subsingleton, not_subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
⊢ I ≠ ⊤

Tactic:
have hI : I ≠ ⊤ := by
      rintro rfl
      exact not_subsingleton _ ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ≠ ⊤
⊢ Nontrivial.{u_1} (A ⧸ I)

Tactic:
have := Ideal.Quotient.nontrivial_iff.mpr hI
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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)
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}))
⊢ ∃ (r : A[X]), r.degree < g.degree ∧ (Ideal.Quotient.mk (Ideal.span {g}) : (a : A[X]) → A[X] ⧸ Ideal.span {g}) r = f

Tactic:
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f

Premises used: Ideal.Quotient.mk_surjective, rfl
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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}))

Tactic:
⟨f %ₘ g, Polynomial.degree_modByMonic_lt f H.monic, ?_⟩

Premises used: Polynomial.IsDistinguishedAt.monic, Polynomial.modByMonic, And.intro, Polynomial.degree_modByMonic_lt, Exists.intro
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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]
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}))
⊢ ∃ (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:
refine ⟨f %ₘ g, Polynomial.degree_modByMonic_lt f H.monic, ?_⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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]
rw : ∃ (a : A[X]), a * g = f - f %ₘ g
⊢ 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:
rw [Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']

Premises used: Ideal.mem_span_singleton', Ideal.Quotient.mk_eq_mk_iff_sub_mem, Eq.comm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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]
rw : f /ₘ g * g = f - (f - g * (f /ₘ g))
⊢ f /ₘ g * g = f - f %ₘ g

Tactic:
rw [Polynomial.modByMonic_eq_sub_mul_div]

Premises used: Polynomial.modByMonic_eq_sub_mul_div
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 * (f /ₘ g))

Tactic:
ring
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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]
⊢ ∃ (a : A[X]), a * g = f - f %ₘ g

Tactic:
exact ⟨f /ₘ g, by rw [Polynomial.modByMonic_eq_sub_mul_div]; ring⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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)
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})
          (⇑⋯.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}))
⊢ 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

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⟩

Premises used: Polynomial.degree, rfl
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
rwa : 1 ∉ I
rwa₁ rwa₂ rwa₃ rwa₄ : I ≠ ⊤
⊢ ((constantCoeff : (a : A⟦X⟧) → A) 1 : A) ∉ I

Tactic:
rwa [constantCoeff_one, ← Ideal.ne_top_iff_one]

Premises used: Ideal.ne_top_iff_one, PowerSeries.constantCoeff_one
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 : A⟦X⟧) = (↑g : A⟦X⟧) * 1

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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_1 : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
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 ⋯
⊢ 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:
convert!
        H.degree_eq_coe_lift_order_map g 1 (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one])
          (by simp)

Premises used: Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
⊢ (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 ⋯

Tactic:
(ENat.lift_eq_toNat_of_lt_top _).symm

Premises used: ENat.lift_eq_toNat_of_lt_top, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
⊢ (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 ⋯

Tactic:
exact (ENat.lift_eq_toNat_of_lt_top _).symm

Premises used: ENat.lift_eq_toNat_of_lt_top, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)

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
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
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}) (⋯.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}))
⊢ 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}))

Tactic:
dsimp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
inr : ∃ (a : A[X]), a * g = ⋯.mod (↑f : A⟦X⟧) - f
⊢ 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}))

Tactic:
rw [Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']

Premises used: Ideal.mem_span_singleton', Ideal.Quotient.mk_eq_mk_iff_sub_mem
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
⊢ 0 * g = ⋯.mod (↑f : A⟦X⟧) - f

Tactic:
simp [H.isWeierstrassDivisorAt'.mod_coe_eq_self (hfdeg.trans_eq h1)]

Premises used: PowerSeries.IsWeierstrassDivisorAt.mod_coe_eq_self, Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt', LT.lt.trans_eq
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
⊢ ∃ (a : A[X]), a * g = ⋯.mod (↑f : A⟦X⟧) - f

Tactic:
exact ⟨0, by simp [H.isWeierstrassDivisorAt'.mod_coe_eq_self (hfdeg.trans_eq h1)]⟩