awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : f = 0
⊢ ∃ (N : ℤ),
    ∀ (g : K⸨X⸩),
      LE.le (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (g - f) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) →
        ∀ n < N, g.coeff n = 0
have pos : ∀ (x : K⸨X⸩)
  (hg :
    LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ))),
  ∀ n < 0, x.coeff n = 0
Tactic: refine ⟨0, fun x hg ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
⊢ ∀ n < 0, x.coeff n = 0
have hg₁ : LE.le (α := WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: rw [hf, sub_zero] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
⊢ ∃ (N : ℤ),
    ∀ (g : K⸨X⸩),
      LE.le (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (g - f) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) →
        ∀ n < N, g.coeff n = 0
have neg : ∀ (x : K⸨X⸩)
  (hg :
    LE.le (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
        WithZero (Multiplicative ℤ))
      (1 : WithZero (Multiplicative ℤ)))
  (n : ℤ) (hn : n < min (sorry.min (s := Function.support f.coeff) sorry) 0 - 1), x.coeff n = 0
Tactic: refine ⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : ℤ
hn : n < min (⋯.min (s := Function.support f.coeff) ⋯) 0 - 1
⊢ x.coeff n = 0
have neg : f.coeff n = 0
Tactic: rw [eq_coeff_of_valuation_sub_lt K hg (d := 0)]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf_1 : f ∈ S ∩ T
hf : ¬f = 0
x : K⸨X⸩
hg :
  LE.le (α := WithZero (Multiplicative ℤ))
    (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (x - f) :
      WithZero (Multiplicative ℤ))
    (1 : WithZero (Multiplicative ℤ))
n : ℤ
hn : n < min (⋯.min (s := Function.support f.coeff) ⋯) 0 - 1
neg : f.coeff n = 0
⊢ x.coeff n = 0
have neg₁ : n < 0
Tactic: rw [eq_coeff_of_valuation_sub_lt K hg (d := 0)]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
have obtain : ∀ (N : ℤ)
  (hN :
    ∀ (g : K⸨X⸩),
      LE.le (α := WithZero (Multiplicative ℤ))
          (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (g - f) :
            WithZero (Multiplicative ℤ))
          (1 : WithZero (Multiplicative ℤ)) →
        ∀ n < N, g.coeff n = 0),
  ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
Tactic: obtain ⟨N, hN⟩ : ∃ N : ℤ, ∀ g : K⸨X⸩,
    Valued.v (g - f) ≤ 1 → ∀ n < N, g.coeff n = 0 := by
    by_cases hf : f = 0
    · refine ⟨0, fun x hg ↦ ?_⟩
      rw [hf, sub_zero] at hg
      exact (valuation_le_iff_coeff_lt_eq_zero K).mp hg
    · refine ⟨min (f.2.isWF.min (HahnSeries.support_nonempty_iff.mpr hf)) 0 - 1, fun _ hg n hn ↦ ?_⟩
      rw [eq_coeff_of_valuation_sub_lt K hg (d := 0)]
      · exact Function.notMem_support.mp fun h ↦
        f.2.isWF.not_lt_min (HahnSeries.support_nonempty_iff.mpr hf) h
        <| lt_trans hn <| Int.sub_one_lt_iff.mpr <| min_le_left _ _
      exact lt_of_lt_of_le hn <| le_of_lt (Int.sub_one_lt_of_le <| min_le_right _ _)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
have h : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
Tactic: use N
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
have h : S ∩ T ⊆ {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N, f.coeff n = 0) x}
Tactic: apply mem_of_superset (inter_mem hS hT)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
⊢ Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N, f.coeff n = 0) x} g
have h_prod : (f, g) ∈ S ×ˢ T
Tactic: have h_prod : (f, g) ∈ S ×ˢ T := by simp [hf.1, hg.2]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
entourage : Set (K⸨X⸩ × K⸨X⸩) :=
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α :=
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (((Valuation.restrict Valued.v :
              Valuation K⸨X⸩
                (MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
                  (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))) :
            (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
          (P.2 - P.1) :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
      (1 :
        MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
          (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))}
ζ : (MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v)ˣ := Units.mk0 1 ⋯
S : Set K⸨X⸩
hS : S ∈ ℱ
T : Set K⸨X⸩
hT : T ∈ ℱ
H : S ×ˢ T ⊆ entourage
f : K⸨X⸩
hf : f ∈ S ∩ T
N : ℤ
hN :
  ∀ (g : K⸨X⸩),
    LE.le (α := WithZero (Multiplicative ℤ))
        (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (g - f) :
          WithZero (Multiplicative ℤ))
        (1 : WithZero (Multiplicative ℤ)) →
      ∀ n < N, g.coeff n = 0
g : K⸨X⸩
hg : g ∈ S ∩ T
h_prod : (f, g) ∈ S ×ˢ T
⊢ Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N, f.coeff n = 0) x} g
have h : LT.lt (α := WithZero (Multiplicative ℤ))
  (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (g - f) :
    WithZero (Multiplicative ℤ))
  (1 : WithZero (Multiplicative ℤ))
Tactic: refine hN g (le_of_lt ?_)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x : UniformSpace K := ⊥
⊢ ∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0
have obtain : ∀ (N : ℤ) (hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0), ∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0
Tactic: obtain ⟨N, hN⟩ := exists_lb_eventual_support hℱ
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
⊢ ∃ (N : ℤ), ∀ n < N, coeff hℱ n = 0
have refine : ∀ (n : ℤ) (hn : n < N), LE.le (α := Filter K) (Filter.map (fun (f : K⸨X⸩) ↦ f.coeff n) ℱ) (pure 0)
Tactic: refine ⟨N, fun n hn ↦ Ultrafilter.eq_of_le_pure (hℱ.map (uniformContinuous_coeff n)).1
      ((principal_singleton _).symm ▸ coeff_tendsto _ _) ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
x : UniformSpace K := ⊥
N : ℤ
hN : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
n : ℤ
hn : n < N
⊢ LE.le (α := Filter K) (Filter.map (fun (f : K⸨X⸩) ↦ f.coeff n) ℱ) (pure 0)
have simp : Membership.mem (γ := Filter K) (Filter.map (fun (f : K⸨X⸩) ↦ f.coeff n) ℱ) 0
Tactic: simp only [pure_zero, nonpos_iff]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ BddBelow (Function.support (coeff hℱ))
have refine : ∀ (d : ℤ) (hd : d ∈ Function.support (coeff hℱ)), sorry.choose (p := fun (N : ℤ) ↦ ∀ n < N, coeff hℱ n = 0) ≤ d
Tactic: refine ⟨(exists_lb_support hℱ).choose, fun d hd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
d : ℤ
hd : d ∈ Function.support (coeff hℱ)
⊢ ⋯.choose (p := fun (N : ℤ) ↦ ∀ n < N, coeff hℱ n = 0) ≤ d
have by_contra : ∀ (hNd : ¬sorry.choose (p := fun (N : ℤ) ↦ ∀ n < N, coeff hℱ n = 0) ≤ d), False
Tactic: by_contra hNd
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d
have obtain : ∀ (N₁ : ℤ) (hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0) (N₂ : ℤ) (hN₂ : ∀ n < N₂, coeff hℱ n = 0),
  ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d
Tactic: obtain ⟨⟨N₁, hN₁⟩, ⟨N₂, hN₂⟩⟩ := exists_lb_eventual_support hℱ, exists_lb_support hℱ
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d
have refine : ∀ (x : K⸨X⸩) (hf : Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N₁, f.coeff n = 0) x} x) (d : ℤ)
  (hd : d < min N₁ N₂), coeff hℱ d = x.coeff d
Tactic: refine ⟨min N₁ N₂, ℱ.3 hN₁ fun _ hf d hd ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
x : K⸨X⸩
hf : Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N₁, f.coeff n = 0) x} x
d : ℤ
hd : d < min N₁ N₂
⊢ coeff hℱ d = x.coeff d
have rw : coeff hℱ d = 0
Tactic: rw [hf d (lt_of_lt_of_le hd (min_le_left _ _)), hN₂ d (lt_of_lt_of_le hd (min_le_right _ _))]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
N₁ : ℤ
hN₁ : ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N₁, f.coeff n = 0
N₂ : ℤ
hN₂ : ∀ n < N₂, coeff hℱ n = 0
x : K⸨X⸩
hf : Membership.mem (γ := Set K⸨X⸩) {x : K⸨X⸩ | (fun (f : K⸨X⸩) ↦ ∀ n < N₁, f.coeff n = 0) x} x
d : ℤ
hd : d < min N₁ N₂
rw : coeff hℱ d = 0
⊢ coeff hℱ d = x.coeff d
have rw₁ : Eq.{u_2 + 1} (α := K) 0 0
Tactic: rw [hf d (lt_of_lt_of_le hd (min_le_left _ _)), hN₂ d (lt_of_lt_of_le hd (min_le_right _ _))]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
⊢ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < D, coeff hℱ d = f.coeff d
have intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
Tactic: have intersec₁ :
    (⋂ n ∈ Set.Iio D, φ n) ⊆ {x : K⸨X⸩ | ∀ d : ℤ, d < D → coeff hℱ d = x.coeff d} := by
    intro _ hf
    simpa only [Set.mem_iInter] using hf
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
ℱ : Filter K⸨X⸩
hℱ : Cauchy ℱ
D : ℤ
φ : ℤ → Set K⸨X⸩ := fun (d : ℤ) ↦ {f : K⸨X⸩ | coeff hℱ d = f.coeff d}
intersec₁ : Subset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) {x : K⸨X⸩ | ∀ d < D, coeff hℱ d = x.coeff d}
ℓ : ℤ := ⋯.choose (p := fun (N : ℤ) ↦ ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ d < N, coeff hℱ d = f.coeff d)
N : ℤ := max ℓ D
⊢ Superset.{u_2} (α := Set K⸨X⸩) (⋂ n ∈ Set.Iio D, φ n) ((⋂ n ∈ Set.Iio ℓ, φ n) ∩ ⋂ n ∈ Set.Icc ℓ N, φ n)
have simp : ∀ (i : ℤ) (i_1 : i < D), (⋂ (n : ℤ), ⋂ (_ : n < ℓ), φ n) ∩ ⋂ (n : ℤ), ⋂ (_ : ℓ ≤ n ∧ n ≤ N), φ n ⊆ φ i
Tactic: simp only [Set.mem_Iio, Set.mem_Icc, Set.subset_iInter_iff]