awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
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 ℕ)
⊢ f' = g * H.div f' + (↑(H.mod f') : A⟦X⟧)

Tactic:
obtain ⟨hf'1, hf'2⟩ := H.isWeierstrassDivisionAt_div_mod f'

Premises used: PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
⊢ 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

Premises used: add_assoc, eq_sub_iff_add_eq, mul_comm, mul_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
ha₁ : g * (a + H.div f') + (↑(H.mod f') : A⟦X⟧) = g * H.div f + (↑(H.mod f) : A⟦X⟧)
⊢ (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:
rw [eq_sub_iff_add_eq, hf2, hf'2, ← add_assoc, mul_comm, ← mul_add] at ha

Premises used: add_assoc, eq_sub_iff_add_eq, mul_comm, mul_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
ha₁ : g * (a + H.div f') + (↑(H.mod f') : A⟦X⟧) = g * H.div f + (↑(H.mod f) : A⟦X⟧)
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 ℕ)
⊢ f = 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

Premises used: add_assoc, eq_sub_iff_add_eq, mul_comm, mul_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
ha₁ : g * (a + H.div f') + (↑(H.mod f') : A⟦X⟧) = g * H.div f + (↑(H.mod f) : A⟦X⟧)
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⟧)
⊢ (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:
rw [eq_sub_iff_add_eq, hf2, hf'2, ← add_assoc, mul_comm, ← mul_add] at ha

Premises used: add_assoc, eq_sub_iff_add_eq, mul_comm, mul_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)
ha₁ : g * (a + H.div f') + (↑(H.mod f') : A⟦X⟧) = g * H.div f + (↑(H.mod f) : A⟦X⟧)
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 ℕ)
⊢ f' = 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

Premises used: add_assoc, eq_sub_iff_add_eq, mul_comm, mul_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 : g * (a + H.div f') + (↑(H.mod f') : A⟦X⟧) = g * H.div f + (↑(H.mod f) : A⟦X⟧)
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')

Tactic:
(H.eq_of_mul_add_eq_mul_add hf'1 hf1 ha).2.symm

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, And.right, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 : g * (a + H.div f') + (↑(H.mod f') : A⟦X⟧) = g * H.div f + (↑(H.mod f) : A⟦X⟧)
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')

Tactic:
exact (H.eq_of_mul_add_eq_mul_add hf'1 hf1 ha).2.symm

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, And.right, Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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})
obtain :
  ∀ (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')
⊢ 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')

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 : 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⟧
obtain :
  ∀ (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})) (β :=
          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) ⋯
          ((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) ⋯
          ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f'))
⊢ 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')

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 : 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⟧
⊢ Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯
      (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) ⋯
        ((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) ⋯
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f'))

Tactic:
H.mod_add f f'

Premises used: PowerSeries.IsWeierstrassDivisorAt.mod_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧
⊢ Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯
      (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) ⋯
        ((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) ⋯
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f'))

Tactic:
exact H.mod_add f f'

Premises used: PowerSeries.IsWeierstrassDivisorAt.mod_add
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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})
obtain :
  ∀ (f : A⟦X⟧),
    Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯
        (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) ⋯
          ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f))
⊢ 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)

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 : 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 : A⟦X⟧
⊢ Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯
      (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) ⋯
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f))

Tactic:
H.mod_smul a f

Premises used: PowerSeries.IsWeierstrassDivisorAt.mod_smul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 : A⟦X⟧
⊢ Quotient.lift (fun (f : A⟦X⟧) ↦ H.mod f) ⋯
      (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) ⋯
        ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f))

Tactic:
exact H.mod_smul a f

Premises used: PowerSeries.IsWeierstrassDivisorAt.mod_smul
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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.mod' : (a : A⟦X⟧ ⧸ Ideal.span {g}) → A[X])
      ((Ideal.Quotient.mk (Ideal.span {g}) : (a : A⟦X⟧) → A⟦X⟧ ⧸ Ideal.span {g}) f) =
    H.mod f

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, PowerSeries.IsWeierstrassDivisorAt.mod, _private.Mathlib.RingTheory.PowerSeries.Trunc.0.PowerSeries.trunc_aux, Finset.sum, rfl
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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⟧)).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

Premises used: Polynomial.toPowerSeries, PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
⊢ (↑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

Premises used: Polynomial.toPowerSeries, PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
h2 : (↑r : A⟦X⟧) = g * H.div (↑r : A⟦X⟧) + (↑(H.mod (↑r : A⟦X⟧)) : A⟦X⟧)
⊢ g * H.div (↑r : A⟦X⟧) + (↑(H.mod (↑r : A⟦X⟧)) : A⟦X⟧) = g * 0 + (↑r : A⟦X⟧)

Tactic:
simpa using h2.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
h2 : (↑r : A⟦X⟧) = g * H.div (↑r : A⟦X⟧) + (↑(H.mod (↑r : A⟦X⟧)) : A⟦X⟧)
⊢ H.div (↑r : A⟦X⟧) = 0

Tactic:
exact (H.eq_of_mul_add_eq_mul_add (q := H.div r) (q' := 0) h1 hr (by simpa using h2.symm)).1

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, And.left
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 ℕ)
h2 : (↑r : A⟦X⟧) = g * H.div (↑r : A⟦X⟧) + (↑(H.mod (↑r : A⟦X⟧)) : A⟦X⟧)
⊢ H.mod (↑r : A⟦X⟧) = r

Tactic:
exact (H.eq_of_mul_add_eq_mul_add (q := H.div r) (q' := 0) h1 hr (by simpa using h2.symm)).2

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, And.right
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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})
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}))
⊢ (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

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 : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst_1 : IsAdicComplete I A
f : A⟦X⟧
rw : ∃ (a : A⟦X⟧), a * g = f - (↑(H.mod 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:
rw [mod'_mk_eq_mod, Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']

Premises used: Ideal.mem_span_singleton', PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Eq.comm
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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 = f - (↑(H.mod f) : A⟦X⟧)
⊢ ∃ (a : A⟦X⟧), a * g = f - (↑(H.mod f) : A⟦X⟧)

Tactic:
use H.div f

Premises used: PowerSeries.IsWeierstrassDivisorAt.div
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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₂ h₃ : f = f
⊢ H.div f * g = f - (↑(H.mod f) : A⟦X⟧)

Tactic:
rw [eq_sub_iff_add_eq, mul_comm, (H.isWeierstrassDivisionAt_div_mod f).2.symm]

Premises used: eq_sub_iff_add_eq, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, mul_comm, PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod, 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
a : A[X]
ha : Membership.mem (γ := Submodule A[X] A[X]) (Ideal.span {g}) a
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
⊢ 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

Premises used: Ideal.mem_span_singleton', Iff.mp