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
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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
heq :
  HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) *
          q)
i_1 i : ℕ
succ :
  Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        ((↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) *
          q) :
      A)
⊢ Membership.mem (α := A) (I ^ (k + 1))
    ((coeff i : (a : A⟦X⟧) → A)
        ((↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) *
          q) :
      A)

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- 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 : 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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
heq :
  HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) *
          q)
i_1 i : ℕ
⊢ Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        ((↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) *
          q) :
      A)

Tactic:
coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (fun i ↦ ?_) ih _

Premises used: Set.Mem, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
-- 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 : 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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
heq :
  HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) *
          q)
i_1 i : ℕ
succ :
  ∀ (i : ℕ),
    Membership.mem (α := A) I
      ((coeff i : (a : A⟦X⟧) → A)
          (↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) :
        A)
⊢ Membership.mem (α := A) (I * I ^ k)
    ((coeff i : (a : A⟦X⟧) → A)
        ((↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) *
          q) :
      A)

Tactic:
refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (fun i ↦ ?_) ih _

Premises used: PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal'
-- 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 : 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 ℕ)
k : ℕ
ih : ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((coeff i : (a : A⟦X⟧) → A) q : A)
h1 : ∀ (i : ℕ), Membership.mem (α := A) (I ^ (k + 1)) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A)
heq :
  HPow.hPow (α := A⟦X⟧) X (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat *
      q =
    (↑⋯.unit⁻¹ : A⟦X⟧) *
      ((↑r : A⟦X⟧) -
        (↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                  (a : A⟦X⟧) → A[X])
                g) :
            A⟦X⟧) *
          q)
i_1 i_2 i : ℕ
succ :
  Polynomial.coeff
      ((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
          (a : A⟦X⟧) → A[X])
        g)
      i ∈
    I
⊢ Membership.mem (α := A) I
    ((coeff i : (a : A⟦X⟧) → A)
        (↑((trunc (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat :
                (a : A⟦X⟧) → A[X])
              g) :
          A⟦X⟧) :
      A)

Tactic:
simp_rw [Polynomial.coeff_coe, g.coeff_trunc_order_mem]

Premises used: Polynomial.coeff_coe, _private.0.PowerSeries.coeff_trunc_order_mem
-- 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 : 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)
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)
⊢ ∀ (i : ℕ), Membership.mem (α := A) (I ^ k) ((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]

Premises used: add_mul, PowerSeries.coeff_mul_mem_ideal_of_coeff_right_mem_ideal', map_sub, Ideal.Quotient.mk, mul_assoc, eq_sub_iff_add_eq, PowerSeries.X, PowerSeries.eq_X_pow_mul_shift_add_trunc, PowerSeries.map, HPow.hPow, PowerSeries.order, mul_comm, ENat.toNat, IsUnit.val_inv_mul, DFunLike.coe, pow_succ', Polynomial.coeff_coe, one_mul, _private.0.PowerSeries.coeff_trunc_order_mem
-- 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 : 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 = g * q' + (↑r' : A⟦X⟧) - (↑r : A⟦X⟧)

Tactic:
rw [← eq_sub_iff_add_eq] at heq

Premises used: eq_sub_iff_add_eq
-- 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 : 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⟧)
rw : g * q' + (↑r' : A⟦X⟧) - (↑r : A⟦X⟧) - g * q' = (↑r' : A⟦X⟧) - (↑r : A⟦X⟧)
⊢ g * (q - q') = (↑(r' - r) : A⟦X⟧)

Tactic:
rw [Polynomial.coe_sub, mul_sub, heq]

Premises used: mul_sub, Polynomial.coe_sub
-- 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 : 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' + (↑r' : A⟦X⟧) - (↑r : A⟦X⟧) - g * q' = (↑r' : A⟦X⟧) - (↑r : A⟦X⟧)

Tactic:
ring
-- 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 : 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⟧)

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
-- 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 : 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' = 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
-- 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 : 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

Tactic:
simp_rw [sub_eq_zero] at h

Premises used: sub_eq_zero
-- 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 : 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' ∧ r' = r
⊢ q = q' ∧ r = r'

Tactic:
⟨h.1, h.2.symm⟩

Premises used: And.right, And.left, And.intro, 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 : 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' ∧ r' = r
⊢ q = q' ∧ r = r'

Tactic:
exact ⟨h.1, h.2.symm⟩
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
⊢ (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')
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
⊢ (f + f').IsWeierstrassDivisionAt g (H.div (f + f')) (H.mod (f + f')) I

Tactic:
have H2 := H.isWeierstrassDivisionAt_div_mod (f + f')
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
H2 : (f + f').IsWeierstrassDivisionAt g (H.div (f + f')) (H.mod (f + f')) I
⊢ H.div (f + f') = H.div f + H.div f'

Tactic:
(H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).1

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, And.left, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
H2 : (f + f').IsWeierstrassDivisionAt g (H.div (f + f')) (H.mod (f + f')) I
⊢ H.div (f + f') = H.div f + H.div f'

Tactic:
exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).1

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, And.left, Eq.symm, Eq.trans
-- 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 : A⟦X⟧
inst_1 : IsAdicComplete I A
⊢ (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I

Tactic:
have H1 := (H.isWeierstrassDivisionAt_div_mod f).smul a
-- 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 : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
⊢ (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I

Tactic:
have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)
-- 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 : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
H2 : (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I
⊢ H.div (a • f) = a • H.div f

Tactic:
(H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).1

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, And.left, Eq.symm, Eq.trans
-- 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 : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
H2 : (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I
⊢ H.div (a • f) = a • H.div f

Tactic:
exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).1

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, And.left, Eq.symm, Eq.trans
-- 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
⊢ H.div 0 = 0

Tactic:
simpa using H.div_smul 0 0

Premises used: PowerSeries.IsWeierstrassDivisorAt.div_smul, OfNat.ofNat
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
H2 : (f + f').IsWeierstrassDivisionAt g (H.div (f + f')) (H.mod (f + f')) I
⊢ H.mod (f + f') = H.mod f + H.mod f'

Tactic:
(H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).2

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, And.right, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
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
H2 : (f + f').IsWeierstrassDivisionAt g (H.div (f + f')) (H.mod (f + f')) I
⊢ H.mod (f + f') = H.mod f + H.mod f'

Tactic:
exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).2

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, And.right, Eq.symm, Eq.trans
-- 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 : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
H2 : (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I
⊢ H.mod (a • f) = a • H.mod f

Tactic:
(H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).2

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, And.right, Eq.symm, Eq.trans
-- 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 : A⟦X⟧
inst_1 : IsAdicComplete I A
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
H2 : (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I
⊢ H.mod (a • f) = a • H.mod f

Tactic:
exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).2

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, And.right, Eq.symm, Eq.trans
-- 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
⊢ H.mod 0 = 0

Tactic:
simpa using H.mod_smul 0 0

Premises used: PowerSeries.IsWeierstrassDivisorAt.mod_smul, OfNat.ofNat
-- 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⟧
hf : f ≈ f'
⊢ Membership.mem (γ := Submodule A⟦X⟧ A⟦X⟧) (Ideal.span {g}) (f - f')

Tactic:
have hf := (Submodule.quotientRel_def (p := Ideal.span {g})).mp hf
-- 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⟧
hf_1 : f ≈ f'
hf : Membership.mem (γ := Submodule A⟦X⟧ A⟦X⟧) (Ideal.span {g}) (f - f')
⊢ ∃ (a : A⟦X⟧), a * g = f - f'

Tactic:
rw [Ideal.mem_span_singleton'] at hf

Premises used: Ideal.mem_span_singleton'
-- 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⟧
hf_1 : f ≈ f'
hf : ∃ (a : A⟦X⟧), a * g = f - f'
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')
⊢ 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
-- 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'
⊢ (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

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 ℕ)
⊢ f = g * H.div f + (↑(H.mod f) : A⟦X⟧)

Tactic:
obtain ⟨hf1, hf2⟩ := 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⟧)
⊢ (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'

Premises used: PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod