awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
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
⊢ f /ʷ 0 = 0
have rw₁ : Eq.{u_1 + 1} (α := A⟦X⟧) 0 0
Tactic: rw [weierstrassDiv, dif_neg (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ Eq (α := A[X]) (f %ʷ 0) 0
have rw : Eq.{u_1 + 1} (α := A[X])
  (if hg :
      Ne (α := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) 0 :
          (IsLocalRing.ResidueField A)⟦X⟧)
        (0 : (IsLocalRing.ResidueField A)⟦X⟧) then
    IsWeierstrassDivisorAt.mod sorry f
  else 0)
  0
Tactic: rw [weierstrassMod, dif_neg (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
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
⊢ Eq (α := A[X]) (f %ʷ 0) 0
have rw₁ : Eq.{u_1 + 1} (α := A[X]) 0 0
Tactic: rw [weierstrassMod, dif_neg (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f g : A⟦X⟧
inst_2 : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ 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 ℕ)
have 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 sorry f).degree <
    (↑(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
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 ℕ)
⊢ 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 ℕ)
have 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 ℕ)
Tactic: split_ifs with hg
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
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⟧)
⊢ 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 ℕ)
have inst : Nontrivial A
Tactic: nontriviality A
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 (f /ʷ g) (f %ʷ g)
have simp_rw : f.IsWeierstrassDivision g (IsWeierstrassDivisorAt.div sorry f) (IsWeierstrassDivisorAt.mod sorry f)
Tactic: simp_rw [weierstrassDiv, weierstrassMod, dif_pos hg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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 * (f /ʷ g) + (↑(f %ʷ g) : A⟦X⟧)
have simp_rw : f = g * IsWeierstrassDivisorAt.div sorry f + (↑(IsWeierstrassDivisorAt.mod sorry f) : A⟦X⟧)
Tactic: simp_rw [weierstrassDiv, weierstrassMod, dif_pos hg]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f f' g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) 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 + 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)
have 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 sorry (f + f') = IsWeierstrassDivisorAt.div sorry f + IsWeierstrassDivisorAt.div sorry f'
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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'
⊢ (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)
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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
⊢ (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)
have 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 sorry (a • f) = a • IsWeierstrassDivisorAt.div sorry f
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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
⊢ (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)
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ 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
have 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 sorry 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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
⊢ 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
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
f f' g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) 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 + 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.mod ⋯ 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.mod ⋯ f'
      else 0)
have 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.mod sorry (f + f') = IsWeierstrassDivisorAt.mod sorry f + IsWeierstrassDivisorAt.mod sorry f'
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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.mod ⋯ (f + f') = IsWeierstrassDivisorAt.mod ⋯ f + IsWeierstrassDivisorAt.mod ⋯ f'
⊢ (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 + 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.mod ⋯ 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.mod ⋯ f'
      else 0)
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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
⊢ (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 ⋯ (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.mod ⋯ f
      else 0)
have 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.mod sorry (a • f) = a • IsWeierstrassDivisorAt.mod sorry f
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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.mod ⋯ (a • f) = a • IsWeierstrassDivisorAt.mod ⋯ f
⊢ (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 ⋯ (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.mod ⋯ f
      else 0)
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g : A⟦X⟧
inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A
⊢ 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.mod ⋯ 0
    else 0)
    0
have 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.mod sorry 0 = 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
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.mod ⋯ 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.mod ⋯ 0
    else 0)
    0
have 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
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ Ne (α := (A ⧸ I)⟦X⟧) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g : (A ⧸ I)⟦X⟧) (0 : (A ⧸ I)⟦X⟧)
have this : Nontrivial.{u_1} (A ⧸ I)
Tactic: have := Ideal.Quotient.nontrivial_iff.mpr hI
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
this : Nontrivial.{u_1} (A ⧸ I)
⊢ Ne (α := (A ⧸ I)⟦X⟧) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g : (A ⧸ I)⟦X⟧) (0 : (A ⧸ I)⟦X⟧)
have rw : ¬(↑(Polynomial.map (Ideal.Quotient.mk I) f) : (A ⧸ I)⟦X⟧) = 0
Tactic: rw [congr(map (Ideal.Quotient.mk I) $(H.eq_mul)), map_mul, ← Polynomial.polynomial_map_coe, ne_eq,
    (H.isUnit.map _).mul_left_eq_zero]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ f.degree =
    (↑((order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).lift ⋯) : WithBot ℕ)
have refine : ((constantCoeff : (a : A⟦X⟧) → A) h : A) ∉ I
Tactic: refine H.isDistinguishedAt.degree_eq_coe_lift_order_map g h ?_ H.eq_mul