awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
⊢ ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)) = f
have refine_1 : ∀ (a : ℕ),
  HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.ofNat a) =
    f.coeff (Int.ofNat a)
Tactic: on_goal 1 => ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
refine_1 :
  ∀ (a : ℕ),
    HahnSeries.coeff
        (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
        (Int.ofNat a) =
      f.coeff (Int.ofNat a)
⊢ ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)) = f
have refine_1₁ : ∀ (n : ℕ),
  HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.negSucc n) =
    f.coeff (Int.negSucc n)
Tactic: on_goal 1 => ext (_ | n)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.negSucc n) =
    f.coeff (Int.negSucc n)
have refine_1 : Eq.{u_2 + 1} (α := K)
  (HahnSeries.coeff
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
    (Int.negSucc n))
  0
Tactic: simp only [h (Int.negSucc n) (Int.negSucc_lt_zero n)]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.negSucc n) =
    f.coeff (Int.negSucc n)
have refine_1 : Eq.{u_2 + 1} (α := K)
  (HahnSeries.coeff
    (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
    (Int.negSucc n))
  0
Tactic: on_goal 1 => simp only [h (Int.negSucc n) (Int.negSucc_lt_zero n)]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
⊢ (∃ (F : K⟦X⟧), ((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F = f) → ∀ n < 0, f.coeff n = 0
have refine_2 : ∀ (F : K⟦X⟧),
  ∀ n < 0, Eq.{u_2 + 1} (α := K) (HahnSeries.coeff (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) n) 0
Tactic: on_goal 2 => rintro ⟨F, rfl⟩ _ _
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ Eq.{u_2 + 1} (α := K)
    (HahnSeries.coeff
      (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) (PowerSeries.mk fun (n : ℕ) ↦ f.coeff (↑n : ℤ)))
      (Int.negSucc n))
    0
have refine_1 : Int.negSucc n ∉
  Set.range (ι := ℕ)
    (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
          { toFun := (⇑(Nat.castAddMonoidHom ℤ) : (a : ℕ) → ℤ), inj' := sorry } sorry) :
      (a : ℕ) → ℤ)
Tactic: apply HahnSeries.embDomain_notin_range
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
f : K⸨X⸩
h : ∀ n < 0, f.coeff n = 0
n : ℕ
⊢ Int.negSucc n ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := (⇑(Nat.castAddMonoidHom ℤ) : (a : ℕ) → ℤ), inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)
have refine_1 : ∀ (x : ℕ), ¬False
Tactic: simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
      Set.mem_range, not_exists, reduceCtorEq]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
n : ℤ
h : n < 0
⊢ Eq.{u_2 + 1} (α := K) (HahnSeries.coeff (((ofPowerSeries ℤ K : K⟦X⟧ →+* K⟦ℤ⟧) : (a : K⟦X⟧) → K⟦ℤ⟧) F) n) 0
have refine_2 : n ∉
  Set.range (ι := ℕ)
    (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
          { toFun := (⇑(Nat.castAddMonoidHom ℤ) : (a : ℕ) → ℤ), inj' := sorry } sorry) :
      (a : ℕ) → ℤ)
Tactic: apply HahnSeries.embDomain_notin_range
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
F : K⟦X⟧
n : ℤ
h : n < 0
⊢ n ∉
    Set.range (ι := ℕ)
      (⇑(RelEmbedding.mk (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℤ) ↦ x1 ≤ x2)
            { toFun := (⇑(Nat.castAddMonoidHom ℤ) : (a : ℕ) → ℤ), inj' := ⋯ } ⋯) :
        (a : ℕ) → ℤ)
have refine_2 : ∀ (x : ℕ), ¬(↑x : ℤ) = n
Tactic: simp only [Nat.coe_castAddMonoidHom, RelEmbedding.coe_mk, Function.Embedding.coeFn_mk,
      Set.mem_range, not_exists, reduceCtorEq]
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
⊢ ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
have pos : ∀ (hn0 : n = 0),
  ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
pos :
  ∀ (hn0 : n = 0),
    ∃ (a : K⸨X⸩),
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
⊢ ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
have neg : ∀ (hn0 : ¬n = 0),
  ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
Tactic: by_cases hn0 : n = 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : n = 0
⊢ ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
have h : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) 0 = n
Tactic: use 0
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
n : WithZero (Multiplicative ℤ)
hn0 : ¬n = 0
⊢ ∃ (a : K⸨X⸩),
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) a = n
have h : ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
    ((single (-n.log) : (a : K) → K⟦ℤ⟧) 1) =
  n
Tactic: use ((HahnSeries.single (-WithZero.log n)) 1)
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
⊢ UniformContinuous (β := K) fun (f : K⸨X⸩) ↦ f.coeff d
have refine : ∀ (S : Set (K × K)) (hS : S ∈ uniformity K),
  ∃ (v : Set (K⸨X⸩ × K⸨X⸩)),
    Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) v ∧ ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S
Tactic: refine uniformContinuous_iff_eventually.mpr fun S hS ↦ eventually_iff_exists_mem.mpr ?_
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
⊢ ∃ (v : Set (K⸨X⸩ × K⸨X⸩)),
    Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩) v ∧ ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S
have h : Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
    {P : K⸨X⸩ × K⸨X⸩ |
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (P.2 - P.1) <
        (↑γ : WithZero (Multiplicative ℤ))} ∧
  ∀ (y : K⸨X⸩ × K⸨X⸩),
    Membership.mem (γ := Set (K⸨X⸩ × K⸨X⸩))
        {P : K⸨X⸩ × K⸨X⸩ |
          ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
              (P.2 - P.1) <
            (↑γ : WithZero (Multiplicative ℤ))}
        y →
      (y.1.coeff d, y.2.coeff d) ∈ S
Tactic: use {P | Valued.v (P.snd - P.fst) < ↑γ}
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
⊢ Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
      {P : K⸨X⸩ × K⸨X⸩ |
        ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (P.2 - P.1) <
          (↑γ : WithZero (Multiplicative ℤ))} ∧
    ∀ (y : K⸨X⸩ × K⸨X⸩),
      Membership.mem (γ := Set (K⸨X⸩ × K⸨X⸩))
          {P : K⸨X⸩ × K⸨X⸩ |
            ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
                (P.2 - P.1) <
              (↑γ : WithZero (Multiplicative ℤ))}
          y →
        (y.1.coeff d, y.2.coeff d) ∈ S
have h : Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
  {P : K⸨X⸩ × K⸨X⸩ |
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) (P.2 - P.1) <
      (↑γ : WithZero (Multiplicative ℤ))}
Tactic: refine ⟨?_, fun _ hP ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
h :
  Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
    {P : K⸨X⸩ × K⸨X⸩ |
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (P.2 - P.1) <
        (↑γ : WithZero (Multiplicative ℤ))}
⊢ Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
      {P : K⸨X⸩ × K⸨X⸩ |
        ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (P.2 - P.1) <
          (↑γ : WithZero (Multiplicative ℤ))} ∧
    ∀ (y : K⸨X⸩ × K⸨X⸩),
      Membership.mem (γ := Set (K⸨X⸩ × K⸨X⸩))
          {P : K⸨X⸩ × K⸨X⸩ |
            ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
                (P.2 - P.1) <
              (↑γ : WithZero (Multiplicative ℤ))}
          y →
        (y.1.coeff d, y.2.coeff d) ∈ S
have h₁ : ∀ (x : K⸨X⸩ × K⸨X⸩)
  (hP :
    Membership.mem (γ := Set (K⸨X⸩ × K⸨X⸩))
      {P : K⸨X⸩ × K⸨X⸩ |
        ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
            (P.2 - P.1) <
          (↑γ : WithZero (Multiplicative ℤ))}
      x),
  (x.1.coeff d, x.2.coeff d) ∈ S
Tactic: refine ⟨?_, fun _ hP ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
⊢ Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
    {P : K⸨X⸩ × K⸨X⸩ |
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (P.2 - P.1) <
        (↑γ : WithZero (Multiplicative ℤ))}
have h : ∀ (x : K⸨X⸩)
  (hx :
    ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x =
      (↑γ : WithZero (Multiplicative ℤ))),
  Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
    {P : K⸨X⸩ × K⸨X⸩ |
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (P.2 - P.1) <
        (↑γ : WithZero (Multiplicative ℤ))}
Tactic: obtain ⟨x, hx⟩ := LaurentSeries.valuation_surjective K γ
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (hypothesis)
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x =
    (↑γ : WithZero (Multiplicative ℤ))
⊢ Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
    {P : K⸨X⸩ × K⸨X⸩ |
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (P.2 - P.1) <
        (↑γ : WithZero (Multiplicative ℤ))}
have this : Ne (α :=
  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 ℤ)))
      x :
    MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
  (0 :
    MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
      (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
Tactic: have : Valued.v.restrict x ≠ 0 := fun h ↦ NeZero.ne γ.1 <|
      hx ▸ MonoidWithZeroHom.ValueGroup₀.restrict₀_eq_zero_iff.1 h
-- Lean 4 proof step from Mathlib.RingTheory.LaurentSeries (goal)
Goal:
K : Type u_2
inst : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : (WithZero (Multiplicative ℤ))ˣ := Units.mk0 (exp (-(d + 1))) ⋯
x : K⸨X⸩
hx :
  ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ)) x =
    (↑γ : WithZero (Multiplicative ℤ))
this :
  Ne (α :=
    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 ℤ)))
        x :
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
    (0 :
      MonoidWithZeroHom.ValueGroup₀ (F := K⸨X⸩ →*₀ WithZero (Multiplicative ℤ))
        (↑Valued.v : K⸨X⸩ →*₀ WithZero (Multiplicative ℤ)))
⊢ Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
    {P : K⸨X⸩ × K⸨X⸩ |
      ((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (P.2 - P.1) <
        (↑γ : WithZero (Multiplicative ℤ))}
have h : Membership.mem (γ := Filter (K⸨X⸩ × K⸨X⸩)) (uniformity K⸨X⸩)
  {P : K⸨X⸩ × K⸨X⸩ |
    LT.lt (α := WithZero (Multiplicative ℤ))
      (((Valued.v : Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) : (a : K⸨X⸩) → WithZero (Multiplicative ℤ))
          (P.2 - P.1) :
        WithZero (Multiplicative ℤ))
      ((MonoidWithZeroHom.ValueGroup₀.embedding :
            (a : MonoidWithZeroHom.ValueGroup₀ Valued.v) → WithZero (Multiplicative ℤ))
          (((MonoidWithZeroHom.ValueGroup₀.restrict₀ Valued.v :
                  K⸨X⸩ →*₀ MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
                (a : K⸨X⸩) → MonoidWithZeroHom.ValueGroup₀ Valued.v)
              x :
            MonoidWithZeroHom.ValueGroup₀ (F := Valuation K⸨X⸩ (WithZero (Multiplicative ℤ))) Valued.v) :
        WithZero (Multiplicative ℤ))}
Tactic: rw [← hx, ← MonoidWithZeroHom.ValueGroup₀.embedding_restrict₀]
-- 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 ⋯
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
have obtain : ∀ (S : Set K⸨X⸩) (hS : S ∈ ℱ) (T : Set K⸨X⸩) (hT : T ∈ ℱ) (H : S ×ˢ T ⊆ entourage),
  ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
Tactic: obtain ⟨S, ⟨hS, ⟨T, ⟨hT, H⟩⟩⟩⟩ := mem_prod_iff.mp <| Filter.le_def.mp hℱ.2 entourage
    <| (Valued.hasBasis_uniformity K⸨X⸩ ℤᵐ⁰).mem_of_mem (i := ζ) (by tauto)
-- 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
⊢ ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
have obtain : ∀ (f : K⸨X⸩) (hf : f ∈ S ∩ T), ∃ (N : ℤ), ∀ᶠ (f : K⸨X⸩) in ℱ, ∀ n < N, f.coeff n = 0
Tactic: obtain ⟨f, hf⟩ := forall_mem_nonempty_iff_neBot.mpr hℱ.1 (S ∩ T) (inter_mem_iff.mpr ⟨hS, hT⟩)
-- 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 : ℤ),
    ∀ (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 : ∀ (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
Tactic: by_cases hf : f = 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
pos :
  ∀ (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
⊢ ∃ (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 : ∀ (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
Tactic: by_cases hf : f = 0