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
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
hI : I ≠ ⊤
⊢ ((constantCoeff : (a : A⟦X⟧) → A) h : A) ∉ I
have contrapose : ∀ (hI : Membership.mem (α := A) I ((constantCoeff : (a : A⟦X⟧) → A) h : A)), I = ⊤
Tactic: contrapose hI
Cleared hypotheses: 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 ≠ ⊤
⊢ f.natDegree = (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
have rw : WithBot.unbotD 0
    (↑(order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat : WithBot ℕ) =
  (order.{u_1} (R := A ⧸ I) ((map (Ideal.Quotient.mk I) : (a : A⟦X⟧) → (A ⧸ I)⟦X⟧) g)).toNat
Tactic: rw [Polynomial.natDegree, H.degree_eq_coe_lift_order_map_of_ne_top hI,
    ENat.lift_eq_toNat_of_lt_top]
-- 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
inst_1 : IsAdicComplete I A
⊢ Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {g})
have rw : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {(↑f : A⟦X⟧) * h})
Tactic: rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]
-- 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
inst_1 : IsAdicComplete I A
rw : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {(↑f : A⟦X⟧) * h})
⊢ Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {g})
have rw₁ : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {(↑f : A⟦X⟧)})
Tactic: rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]
-- 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
inst_1 : IsAdicComplete I A
x : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})
⊢ Eq (α := Ideal A⟦X⟧) (Ideal.span {g}) (Ideal.span {(↑f : A⟦X⟧)})
have rw : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧) * h}) (Ideal.span {(↑f : A⟦X⟧)})
Tactic: rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]
-- 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
inst_1 : IsAdicComplete I A
x : HasQuotient.Quotient A⟦X⟧ (B := Ideal A⟦X⟧) (Ideal.span {g})
rw : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧) * h}) (Ideal.span {(↑f : A⟦X⟧)})
⊢ Eq (α := Ideal A⟦X⟧) (Ideal.span {g}) (Ideal.span {(↑f : A⟦X⟧)})
have rw₁ : Eq (α := Ideal A⟦X⟧) (Ideal.span {(↑f : A⟦X⟧)}) (Ideal.span {(↑f : A⟦X⟧)})
Tactic: rw [H.eq_mul, Ideal.span_singleton_mul_right_unit H.isUnit]
-- 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
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ g * g' = (↑(f * f') : A⟦X⟧) * (h * h')
have rw : (↑f : A⟦X⟧) * h * ((↑f' : A⟦X⟧) * h') = (↑f : A⟦X⟧) * (↑f' : A⟦X⟧) * (h * h')
Tactic: rw [H.eq_mul, H'.eq_mul, Polynomial.coe_mul]
-- 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
a : A
ha : IsUnit a
⊢ (a • g).IsWeierstrassFactorizationAt f (a • h) I
have refine_1 : IsUnit (a • h)
Tactic: refine ⟨H.isDistinguishedAt, ?_, ?_⟩
-- 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
a : A
ha : IsUnit a
refine_1 : IsUnit (a • h)
⊢ (a • g).IsWeierstrassFactorizationAt f (a • h) I
have refine_2 : a • g = (↑f : A⟦X⟧) * a • h
Tactic: refine ⟨H.isDistinguishedAt, ?_, ?_⟩
-- 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
a : A
ha : IsUnit a
⊢ IsUnit (a • h)
have refine_1 : IsUnit (HMul.hMul (α := A⟦X⟧) ((algebraMap A A⟦X⟧ : (a : A) → A⟦X⟧) a : A⟦X⟧) h)
Tactic: rw [Algebra.smul_def]
-- 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
⊢ IsUnit q
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: obtain ⟨H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat, H2⟩ := H
Cleared hypotheses: H
-- 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
H1 :
  r.degree <
    (↑(order.{u_1} (R := IsLocalRing.ResidueField A)
            ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat :
      WithBot ℕ)
⊢ IsUnit q
have H2 : 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 =
  g * q + (↑r : A⟦X⟧)
Tactic: obtain ⟨H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat, H2⟩ := H
Cleared hypotheses: H
-- 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⟧)
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 : HPow.hPow (α := A⟦X⟧) X n = g * q + (↑r : A⟦X⟧)
⊢ IsUnit q
have H2₁ : Eq (α := IsLocalRing.ResidueField A)
  ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (HPow.hPow (α := A⟦X⟧) X n)) :
    IsLocalRing.ResidueField A)
  ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * q + (↑r : A⟦X⟧))) :
    IsLocalRing.ResidueField A)
Tactic: replace H2 := congr(coeff n (($H2).map (IsLocalRing.residue A)))
Cleared hypotheses: H2
-- 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⟧)
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 (α := IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (HPow.hPow (α := A⟦X⟧) X n)) :
      IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) (g * q + (↑r : A⟦X⟧))) :
      IsLocalRing.ResidueField A)
⊢ IsUnit q
have H2₁ : Eq (α := IsLocalRing.ResidueField A) (1 : IsLocalRing.ResidueField A)
  ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
      (HMul.hMul (α := (IsLocalRing.ResidueField A)⟦X⟧) (β := (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
          (IsLocalRing.ResidueField A)⟦X⟧)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q :
          (IsLocalRing.ResidueField A)⟦X⟧)) :
    IsLocalRing.ResidueField A)
Tactic: simp_rw [map_pow, map_X, coeff_X_pow_self, map_add, map_mul, coeff_map,
    Polynomial.coeff_coe, Polynomial.coeff_eq_zero_of_degree_lt H1, map_zero, add_zero] at H2
Cleared hypotheses: H2
-- 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 (α := IsLocalRing.ResidueField A) (1 : IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        (HMul.hMul (α := (IsLocalRing.ResidueField A)⟦X⟧) (β := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q :
            (IsLocalRing.ResidueField A)⟦X⟧)) :
      IsLocalRing.ResidueField A)
⊢ IsUnit q
have rw : IsUnit (M := IsLocalRing.ResidueField A)
  ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
    IsLocalRing.ResidueField A)
Tactic: rw [isUnit_iff_constantCoeff, ← isUnit_map_iff (IsLocalRing.residue A)]
-- 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 (α := IsLocalRing.ResidueField A) (1 : IsLocalRing.ResidueField A)
    ((coeff n : (a : (IsLocalRing.ResidueField A)⟦X⟧) → IsLocalRing.ResidueField A)
        (HMul.hMul (α := (IsLocalRing.ResidueField A)⟦X⟧) (β := (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g :
            (IsLocalRing.ResidueField A)⟦X⟧)
          ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) q :
            (IsLocalRing.ResidueField A)⟦X⟧)) :
      IsLocalRing.ResidueField A)
⊢ IsUnit (M := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
      IsLocalRing.ResidueField A)
have rw : ∀
  (H2 :
    1 =
      HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A)
        ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
          IsLocalRing.ResidueField A)
        ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((coeff (n, 0).1 : (a : A⟦X⟧) → A) g) :
          IsLocalRing.ResidueField A)),
  IsUnit (M := IsLocalRing.ResidueField A)
    ((IsLocalRing.residue A : (a : A) → IsLocalRing.ResidueField A) ((constantCoeff : (a : A⟦X⟧) → A) q) :
      IsLocalRing.ResidueField A)
Tactic: rw [coeff_mul, ← Finset.sum_subset (s₁ := {(n, 0)}) (by simp) (fun p hp hnotMem ↦ ?_),
    Finset.sum_singleton, coeff_map, coeff_map, coeff_zero_eq_constantCoeff, mul_comm] at H2
Cleared hypotheses: H2
-- 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 ∉ {(n, 0)}
⊢ 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) =
    0
have rw : HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A) (0 : 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) =
  0
Tactic: rw [coeff_of_lt_order p.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⟧)
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 ∉ {(n, 0)}
rw :
  HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A) (0 : 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) =
    0
⊢ 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) =
    0
have rw₁ : (↑p.1 : ℕ∞) <
  order.{u_1} (R := IsLocalRing.ResidueField A)
    ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)
Tactic: rw [coeff_of_lt_order p.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⟧)
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 ∉ {(n, 0)}
⊢ HMul.hMul (α := IsLocalRing.ResidueField A) (β := IsLocalRing.ResidueField A) (0 : 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) =
    0
have rw : Eq.{u_1 + 1} (α := IsLocalRing.ResidueField A) 0 0
Tactic: rw [zero_mul]
-- 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 ∉ {(n, 0)}
⊢ (↑p.1 : ℕ∞) <
    order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)
have rw : p.1 <
  (order.{u_1} (R := IsLocalRing.ResidueField A)
      ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
Tactic: rw [← ENat.lt_lift_iff (h := order_finite_iff_ne_zero.2 hg), ENat.lift_eq_toNat_of_lt_top]
-- 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 ∉ {(n, 0)}
⊢ p.1 <
    (order.{u_1} (R := IsLocalRing.ResidueField A)
        ((map (IsLocalRing.residue A) : (a : A⟦X⟧) → (IsLocalRing.ResidueField A)⟦X⟧) g)).toNat
have refine : p.1 ≠ n
Tactic: refine (Finset.antidiagonal.fst_le hp).lt_of_ne ?_
-- 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 ∉ {(n, 0)}
⊢ p.1 ≠ n
have contrapose : ∀ (hnotMem : p.1 = n), Membership.mem (γ := Finset (ℕ × ℕ)) {(n, 0)} p
Tactic: contrapose hnotMem
Cleared hypotheses: hnotMem