-- Mathlib/RingTheory/LaurentSeries.lean
theorem coe_range_dense : DenseRange ((↑) : RatFunc K → K⸨X⸩)

Proof state:
case h.intro.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Tactic:
obtain ⟨γ, hγ⟩ := Valued.mem_nhds_zero.mp hT₀

Result:
case h.intro.intro.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Proof state:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : V ∈ uniformity K⸨X⸩
h_symm : SymmetricRel V
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Tactic:
rw [uniformity_eq_comap_neg_add_nhds_zero_swapped] at hV

Result:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : V ∈ Filter.comap (fun x => -x.2 + x.1) (nhds 0)
h_symm : SymmetricRel V
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Proof state:
case h.intro.intro.intro.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
P : RatFunc K
h✝ : Valued.v (f - ↑P) < ↑γ
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Tactic:
use P

Result:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
P : RatFunc K
h✝ : Valued.v (f - ↑P) < ↑γ
⊢ ↑P ∈ UniformSpace.ball f V

Proof state:
case h.a.a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
P : RatFunc K
h✝ : Valued.v (f - ↑P) < ↑γ
⊢ (fun x => -x.2 + x.1) (f, ↑P) ∈ {x | Valued.v x < ↑γ}

Tactic:
simpa only [add_comm, ← sub_eq_add_neg, gt_iff_lt, Set.mem_setOf_eq]

Result:
no goals

Proof state:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ ∀ {V : Set (K⸨X⸩ × K⸨X⸩)}, V ∈ uniformity K⸨X⸩ → SymmetricRel V → ∃ a, ↑a ∈ UniformSpace.ball f V

Tactic:
intro V hV h_symm

Result:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : V ∈ uniformity K⸨X⸩
h_symm : SymmetricRel V
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Proof state:
K : Type u_2
inst✝ : Field K
⊢ DenseRange RatFunc.coeToLaurentSeries_fun

Tactic:
rw [denseRange_iff_closure_range]

Result:
K : Type u_2
inst✝ : Field K
⊢ closure (Set.range RatFunc.coeToLaurentSeries_fun) = Set.univ

Proof state:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
P : RatFunc K
h✝ : Valued.v (f - ↑P) < ↑γ
⊢ ↑P ∈ UniformSpace.ball f V

Tactic:
apply hT₁

Result:
case h.a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
P : RatFunc K
h✝ : Valued.v (f - ↑P) < ↑γ
⊢ (f, ↑P) ∈ (fun x => -x.2 + x.1) ⁻¹' T

Proof state:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
hV : V ∈ Filter.comap (fun x => -x.2 + x.1) (nhds 0)
h_symm : SymmetricRel V
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Tactic:
obtain ⟨T, hT₀, hT₁⟩ := hV

Result:
case h.intro.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Proof state:
K : Type u_2
inst✝ : Field K
⊢ closure (Set.range RatFunc.coeToLaurentSeries_fun) = Set.univ

Tactic:
ext f

Result:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ f ∈ closure (Set.range RatFunc.coeToLaurentSeries_fun) ↔ f ∈ Set.univ

Proof state:
case h.intro.intro.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Tactic:
obtain ⟨P, _⟩ := exists_ratFunc_val_lt f γ

Result:
case h.intro.intro.intro.intro
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
P : RatFunc K
h✝ : Valued.v (f - ↑P) < ↑γ
⊢ ∃ a, ↑a ∈ UniformSpace.ball f V

Proof state:
case h.a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
P : RatFunc K
h✝ : Valued.v (f - ↑P) < ↑γ
⊢ (f, ↑P) ∈ (fun x => -x.2 + x.1) ⁻¹' T

Tactic:
apply hγ

Result:
case h.a.a
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
V : Set (K⸨X⸩ × K⸨X⸩)
h_symm : SymmetricRel V
T : Set K⸨X⸩
hT₀ : T ∈ nhds 0
hT₁ : (fun x => -x.2 + x.1) ⁻¹' T ⊆ V
γ : ℤₘ₀ˣ
hγ : {x | Valued.v x < ↑γ} ⊆ T
P : RatFunc K
h✝ : Valued.v (f - ↑P) < ↑γ
⊢ (fun x => -x.2 + x.1) (f, ↑P) ∈ {x | Valued.v x < ↑γ}

Proof state:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ f ∈ closure (Set.range RatFunc.coeToLaurentSeries_fun) ↔ f ∈ Set.univ

Tactic:
simp only [UniformSpace.mem_closure_iff_symm_ball, Set.mem_univ, iff_true, Set.Nonempty,
  Set.mem_inter_iff, Set.mem_range, Set.mem_setOf_eq, exists_exists_eq_and]

Result:
case h
K : Type u_2
inst✝ : Field K
f : K⸨X⸩
⊢ ∀ {V : Set (K⸨X⸩ × K⸨X⸩)}, V ∈ uniformity K⸨X⸩ → SymmetricRel V → ∃ a, ↑a ∈ UniformSpace.ball f V