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
g q : A⟦X⟧
r : 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⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p.1 = n
⊢ Membership.mem (γ := Finset (ℕ × ℕ)) {(n, 0)} p
have rwa : p = (n, 0)
Tactic: rwa [Finset.mem_singleton, Finset.antidiagonal_congr hp (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H1 : r.degree < (↑n : WithBot ℕ)
H2 :
  Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 1
    (∑ p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n,
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((coeff p.1 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g) :
          IsLocalRing.ResidueField A)
        ((coeff p.2 : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q) :
          IsLocalRing.ResidueField A))
p : ℕ × ℕ
hp : p ∈ @Finset.antidiagonal _ Nat.instAddMonoid _ n
hnotMem : p.1 = n
rwa : p = (n, 0)
⊢ Membership.mem (γ := Finset (ℕ × ℕ)) {(n, 0)} p
have rwa₁ : p.1 = (n, 0).1
Tactic: rwa [Finset.mem_singleton, Finset.antidiagonal_congr hp (by simp)]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
⊢ g.IsWeierstrassFactorization
    (HPow.hPow (α := A[X]) Polynomial.X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat -
      r)
    (↑⋯.unit⁻¹ : A⟦X⟧)
have H1 : r.degree <
  (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
    WithBot ℕ)
Tactic: have H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat := H.1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
H1 :
  r.degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)
⊢ g.IsWeierstrassFactorization
    (HPow.hPow (α := A[X]) Polynomial.X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat -
      r)
    (↑⋯.unit⁻¹ : A⟦X⟧)
have set : let n :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat;
∀ (H_1 : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r) (H1 : r.degree < (↑n : WithBot ℕ)),
  g.IsWeierstrassFactorization (HPow.hPow (α := A[X]) Polynomial.X n - r) (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: set n := (g.map (IsLocalRing.residue A)).order.toNat
Cleared hypotheses: H1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
H1 : r.degree < (↑n : WithBot ℕ)
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
⊢ g.IsWeierstrassFactorization f (↑⋯.unit⁻¹ : A⟦X⟧)
have H1₁ : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
Tactic: replace H1 : r.degree < (Polynomial.X (R := A) ^ n).degree := by rwa [Polynomial.degree_X_pow]
Cleared hypotheses: H1
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
this : f.degree = (↑n : WithBot ℕ)
⊢ f.natDegree = n
have rw : WithBot.unbotD 0 (↑n : WithBot ℕ) = n
Tactic: rw [Polynomial.natDegree, this]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
⊢ f.natDegree = n
have suffices : f.degree = (↑n : WithBot ℕ)
Tactic: suffices f.degree = n by rw [Polynomial.natDegree, this]; rfl
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
⊢ f.degree = (↑n : WithBot ℕ)
have rw : (HPow.hPow (α := A[X]) Polynomial.X n).degree = (↑n : WithBot ℕ)
Tactic: rw [Polynomial.degree_sub_eq_left_of_degree_lt H1, Polynomial.degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
rw : (HPow.hPow (α := A[X]) Polynomial.X n).degree = (↑n : WithBot ℕ)
⊢ f.degree = (↑n : WithBot ℕ)
have rw₁ : Eq (α := WithBot ℕ) (↑n : WithBot ℕ) (↑n : WithBot ℕ)
Tactic: rw [Polynomial.degree_sub_eq_left_of_degree_lt H1, Polynomial.degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
⊢ g.IsWeierstrassFactorization f (↑⋯.unit⁻¹ : A⟦X⟧)
have hfdeg : f.natDegree = n
Tactic: have hfdeg : f.natDegree = n := by
    suffices f.degree = n by rw [Polynomial.natDegree, this]; rfl
    rw [Polynomial.degree_sub_eq_left_of_degree_lt H1, Polynomial.degree_X_pow]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
⊢ g.IsWeierstrassFactorization f (↑⋯.unit⁻¹ : A⟦X⟧)
have refine_1 : ∀ {i : ℕ} (hi : i < f.natDegree), Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (f.coeff i)
Tactic: refine ⟨⟨⟨fun {i} hi ↦ ?_⟩, .sub_of_left (Polynomial.monic_X_pow _) H1⟩, Units.isUnit _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
refine_1 : ∀ {i : ℕ} (hi : i < f.natDegree), Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (f.coeff i)
⊢ g.IsWeierstrassFactorization f (↑⋯.unit⁻¹ : A⟦X⟧)
have refine_2 : g = (↑f : A⟦X⟧) * (↑sorry.unit⁻¹ : A⟦X⟧)
Tactic: refine ⟨⟨⟨fun {i} hi ↦ ?_⟩, .sub_of_left (Polynomial.monic_X_pow _) H1⟩, Units.isUnit _, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < f.natDegree
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (f.coeff i)
have hi₁ : i < n
Tactic: rw [hfdeg] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (f.coeff i)
have refine_1 : Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
Tactic: simp_rw [f, Polynomial.coeff_sub, Polynomial.coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff]
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (hypothesis)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
have this : Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
  ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) : A)
Tactic: have := H.coeff_f_sub_r_mem hi
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
this :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) : A)
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
have refine_1 : ∀
  (this :
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
      (HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n) : A)
        ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
Tactic: rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
this :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) : A)
refine_1 :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n) : A)
          ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
have refine_1₁ : ∀
  (this :
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
      (HSub.hSub (α := A) (β := A) (if i = n then 1 else 0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
Tactic: rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.PowerSeries.WeierstrassPreparation (goal)
Goal:
A : Type u_1
inst : CommRing A
inst_1 : IsLocalRing A
g q : A⟦X⟧
r : 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⟧)
H_1 :
  (HPow.hPow (α := A⟦X⟧) X
        (order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧)
              g)).toNat).IsWeierstrassDivision
    g q r
n : ℕ :=
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
H : (HPow.hPow (α := A⟦X⟧) X n).IsWeierstrassDivision g q r
f : A[X] := HPow.hPow (α := A[X]) Polynomial.X n - r
H1 : r.degree < (HPow.hPow (α := A[X]) Polynomial.X n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
this :
  Membership.mem (α := A) (γ := Ideal A) (IsLocalRing.maximalIdeal A)
    ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n - (↑r : A⟦X⟧)) : A)
refine_1 :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) ((coeff i : (a : A⟦X⟧) → A) (HPow.hPow (α := A⟦X⟧) X n) : A)
          ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
refine_1₁ :
  ∀
    (this :
      Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
        (HSub.hSub (α := A) (β := A) (if i = n then 1 else 0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
⊢ Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
have refine_1₂ : ∀
  (this :
    Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A)
      (HSub.hSub (α := A) (β := A) (0 : A) ((coeff i : (a : A⟦X⟧) → A) (↑r : A⟦X⟧) : A))),
  Membership.mem (γ := Ideal A) (IsLocalRing.maximalIdeal A) (r.coeff i)
Tactic: rwa [map_sub, coeff_X_pow, if_neg hi.ne, zero_sub, neg_mem_iff, Polynomial.coeff_coe] at this
Cleared hypotheses: this