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
f : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {(↑g : 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⟧)}))
      (Function.comp (β := 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]) f) =
    f

Tactic:
H.isWeierstrassDivisorAt'.mk_mod'_eq_self

Premises used: Quotient.liftOn', AddCon.liftOn, Submodule.Quotient.mk, Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt', Polynomial.coeff, Polynomial.toPowerSeries, PowerSeries.mk, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self
-- 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 : 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⟧)}))
      (Function.comp (β := 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]) f) =
    f

Tactic:
exact H.isWeierstrassDivisorAt'.mk_mod'_eq_self

Premises used: Polynomial.IsDistinguishedAt.isWeierstrassDivisorAt', PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ ∃ (q : A⟦X⟧) (r : A[X]), f.IsWeierstrassDivision g q r

Tactic:
⟨_, _, (IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f⟩

Premises used: PowerSeries.IsWeierstrassDivisor.of_map_ne_zero, Exists.intro, PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ ¬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⟧)

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
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 ⋯ f
    else 0)
    0
rw₁ rw₂ : Eq.{u_1 + 1} (α := A⟦X⟧) 0 0
⊢ f /ʷ 0 = 0

Tactic:
rw [weierstrassDiv, dif_neg (by simp)]

Premises used: PowerSeries.weierstrassDiv, dif_neg
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
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.mod ⋯ f
    else 0)
    0
rw₁ rw₂ : Eq.{u_1 + 1} (α := A[X]) 0 0
⊢ Eq (α := A[X]) (f %ʷ 0) 0

Tactic:
rw [weierstrassMod, dif_neg (by simp)]

Premises used: dif_neg, PowerSeries.weierstrassMod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
pos :
  ∀
    (hg :
      Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧)),
    (IsWeierstrassDivisorAt.mod ⋯ f).degree <
      (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
              ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
        WithBot ℕ)
neg :
  ∀
    (hg :
      ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          (0 : (IsLocalRing.ResidueField A)⟦X⟧)),
    Polynomial.degree.{u_1} (R := A) 0 <
      (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
              ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
        WithBot ℕ)
⊢ Polynomial.degree.{u_1} (R := A)
      (if hg :
          Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
              (IsLocalRing.ResidueField A)⟦X⟧)
            (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
        IsWeierstrassDivisorAt.mod ⋯ f
      else 0) <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)

Tactic:
split_ifs with hg
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ (IsWeierstrassDivisorAt.mod ⋯ f).degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)

Tactic:
degree_trunc_lt _ _

Premises used: PowerSeries.degree_trunc_lt, PowerSeries.IsWeierstrassDivisorAt.mod, IsLocalRing.ResidueField
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ (IsWeierstrassDivisorAt.mod ⋯ f).degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)

Tactic:
exact degree_trunc_lt _ _

Premises used: PowerSeries.degree_trunc_lt
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
      (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ Nontrivial A

Tactic:
nontriviality A
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
      (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_3 : Nontrivial A
⊢ LT.lt (α := WithBot ℕ) ⊥
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)

Tactic:
WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
      (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_3 : Nontrivial A
⊢ LT.lt (α := WithBot ℕ) ⊥
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)

Tactic:
exact WithBot.bot_lt_coe _

Premises used: WithBot.bot_lt_coe
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
simp_rw : f.IsWeierstrassDivision g (IsWeierstrassDivisorAt.div ⋯ f) (IsWeierstrassDivisorAt.mod ⋯ f)
⊢ f.IsWeierstrassDivision g (f /ʷ g) (f %ʷ g)

Tactic:
simp_rw [weierstrassDiv, weierstrassMod, dif_pos hg]

Premises used: PowerSeries.weierstrassDiv, dif_pos, PowerSeries.weierstrassMod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f.IsWeierstrassDivision g (IsWeierstrassDivisorAt.div ⋯ f) (IsWeierstrassDivisorAt.mod ⋯ f)

Tactic:
(IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f

Premises used: PowerSeries.IsWeierstrassDivisor.of_map_ne_zero, PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f.IsWeierstrassDivision g (IsWeierstrassDivisorAt.div ⋯ f) (IsWeierstrassDivisorAt.mod ⋯ f)

Tactic:
exact (IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f

Premises used: PowerSeries.IsWeierstrassDivisor.of_map_ne_zero, PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
simp_rw : f = g * IsWeierstrassDivisorAt.div ⋯ f + (↑(IsWeierstrassDivisorAt.mod ⋯ f) : A⟦X⟧)
⊢ f = g * (f /ʷ g) + (↑(f %ʷ g) : A⟦X⟧)

Tactic:
simp_rw [weierstrassDiv, weierstrassMod, dif_pos hg]

Premises used: PowerSeries.weierstrassDiv, dif_pos, PowerSeries.weierstrassMod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f = g * IsWeierstrassDivisorAt.div ⋯ f + (↑(IsWeierstrassDivisorAt.mod ⋯ f) : A⟦X⟧)

Tactic:
((IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f).2

Premises used: PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, PowerSeries.IsWeierstrassDivisor.of_map_ne_zero, PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ f = g * IsWeierstrassDivisorAt.div ⋯ f + (↑(IsWeierstrassDivisorAt.mod ⋯ f) : A⟦X⟧)

Tactic:
exact ((IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f).2

Premises used: PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, PowerSeries.IsWeierstrassDivisor.of_map_ne_zero, PowerSeries.IsWeierstrassDivisorAt.isWeierstrassDivisionAt_div_mod
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsHausdorff (IsLocalRing.maximalIdeal A) A
q q' : A⟦X⟧
r r' : A[X]
H : f.IsWeierstrassDivision g q r
H2 : f.IsWeierstrassDivision g q' r'
⊢ q = q' ∧ r = r'

Tactic:
(IsWeierstrassDivisor.of_map_ne_zero hg).eq_of_mul_add_eq_mul_add H.1 H2.1 (H.2.symm.trans H2.2)

Premises used: PowerSeries.IsWeierstrassDivisorAt.eq_of_mul_add_eq_mul_add, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerSeries.IsWeierstrassDivisionAt.eq_mul_add, PowerSeries.IsWeierstrassDivisor.of_map_ne_zero, Eq.symm, Eq.trans
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsHausdorff (IsLocalRing.maximalIdeal A) A
q : A⟦X⟧
r : A[X]
H : IsWeierstrassDivision 0 g q r
⊢ q = 0 ∧ r = 0

Tactic:
H.elim hg (g.isWeierstrassDivisionAt_zero _)

Premises used: PowerSeries.IsWeierstrassDivision.elim, PowerSeries.isWeierstrassDivisionAt_zero
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
hg :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
q : A⟦X⟧
r : A[X]
H : f.IsWeierstrassDivision g q r
⊢ q = f /ʷ g ∧ r = f %ʷ g

Tactic:
H.elim hg (f.isWeierstrassDivision_weierstrassDiv_weierstrassMod hg)

Premises used: PowerSeries.isWeierstrassDivision_weierstrassDiv_weierstrassMod, PowerSeries.IsWeierstrassDivision.elim
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f f' g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
pos :
  ∀
    (h :
      Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧)),
    IsWeierstrassDivisorAt.div ⋯ (f + f') = IsWeierstrassDivisorAt.div ⋯ f + IsWeierstrassDivisorAt.div ⋯ f'
neg :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧) →
    0 = HAdd.hAdd (α := A⟦X⟧) 0 0
⊢ (if hg :
        Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
      IsWeierstrassDivisorAt.div ⋯ (f + f')
    else 0) =
    HAdd.hAdd (α := A⟦X⟧)
      (if hg :
          Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
              (IsLocalRing.ResidueField A)⟦X⟧)
            (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
        IsWeierstrassDivisorAt.div ⋯ f
      else 0)
      (if hg :
          Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
              (IsLocalRing.ResidueField A)⟦X⟧)
            (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
        IsWeierstrassDivisorAt.div ⋯ f'
      else 0)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f f' g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ IsWeierstrassDivisorAt.div ⋯ (f + f') = IsWeierstrassDivisorAt.div ⋯ f + IsWeierstrassDivisorAt.div ⋯ f'

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f f' g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
      (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ 0 = HAdd.hAdd (α := A⟦X⟧) 0 0

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
a : A
f g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
pos :
  ∀
    (h :
      Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧)),
    IsWeierstrassDivisorAt.div ⋯ (a • f) = a • IsWeierstrassDivisorAt.div ⋯ f
neg :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧) →
    0 = HSMul.hSMul (β := A⟦X⟧) a 0
⊢ (if hg :
        Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
      IsWeierstrassDivisorAt.div ⋯ (a • f)
    else 0) =
    HSMul.hSMul (β := A⟦X⟧) a
      (if hg :
          Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
              (IsLocalRing.ResidueField A)⟦X⟧)
            (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
        IsWeierstrassDivisorAt.div ⋯ f
      else 0)

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
a : A
f g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ IsWeierstrassDivisorAt.div ⋯ (a • f) = a • IsWeierstrassDivisorAt.div ⋯ f

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
a : A
f g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
      (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ 0 = HSMul.hSMul (β := A⟦X⟧) a 0

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
pos :
  ∀
    (h :
      Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧)),
    IsWeierstrassDivisorAt.div ⋯ 0 = 0
neg :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧) →
    Eq.{u_1 + 1} (α := A⟦X⟧) 0 0
⊢ Eq.{u_1 + 1} (α := A⟦X⟧)
    (if hg :
        Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
      IsWeierstrassDivisorAt.div ⋯ 0
    else 0)
    0

Tactic:
split_ifs
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
    (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ IsWeierstrassDivisorAt.div ⋯ 0 = 0

Tactic:
simp
-- Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
h :
  ¬Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g : (IsLocalRing.ResidueField A)⟦X⟧)
      (0 : (IsLocalRing.ResidueField A)⟦X⟧)
⊢ Eq.{u_1 + 1} (α := A⟦X⟧) 0 0

Tactic:
simp