-- Mathlib/RingTheory/LaurentSeries.lean
theorem uniformContinuous_coeff {uK : UniformSpace K} (d : ℤ) :
    UniformContinuous fun f : K⸨X⸩ ↦ f.coeff d

Proof state:
case h
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
P : K⸨X⸩ × K⸨X⸩
hP : P ∈ {P | Valued.v (P.2 - P.1) < ↑γ}
⊢ (P.1.coeff d, P.2.coeff d) ∈ S

Tactic:
rw [eq_coeff_of_valuation_sub_lt K (le_of_lt hP) (lt_add_one _)]

Result:
case h
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
P : K⸨X⸩ × K⸨X⸩
hP : P ∈ {P | Valued.v (P.2 - P.1) < ↑γ}
⊢ (P.1.coeff d, P.1.coeff d) ∈ S

Proof state:
case h
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
P : K⸨X⸩ × K⸨X⸩
hP : P ∈ {P | Valued.v (P.2 - P.1) < ↑γ}
⊢ (P.1.coeff d, P.1.coeff d) ∈ S

Tactic:
exact mem_uniformity_of_eq hS rfl

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
⊢ ∃ v ∈ uniformity K⸨X⸩, ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S

Tactic:
use {P | Valued.v (P.snd - P.fst) < ↑γ}

Result:
case h
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
⊢ {P | Valued.v (P.2 - P.1) < ↑γ} ∈ uniformity K⸨X⸩ ∧
    ∀ y ∈ {P | Valued.v (P.2 - P.1) < ↑γ}, (y.1.coeff d, y.2.coeff d) ∈ S

Proof state:
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
⊢ ∃ v ∈ uniformity K⸨X⸩, ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S

Tactic:
let γ : ℤₘ₀ˣ := Units.mk0 (↑(Multiplicative.ofAdd (-(d + 1)))) WithZero.coe_ne_zero

Result:
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
⊢ ∃ v ∈ uniformity K⸨X⸩, ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S

Proof state:
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
⊢ True

Tactic:
tauto

Result:
no goals

Proof state:
case h
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
⊢ {P | Valued.v (P.2 - P.1) < ↑γ} ∈ uniformity K⸨X⸩ ∧
    ∀ y ∈ {P | Valued.v (P.2 - P.1) < ↑γ}, (y.1.coeff d, y.2.coeff d) ∈ S

Tactic:
refine ⟨(Valued.hasBasis_uniformity K⸨X⸩ ℤₘ₀).mem_of_mem (by tauto), fun P hP ↦ ?_⟩

Result:
case h
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
γ : ℤₘ₀ˣ := Units.mk0 ↑(ofAdd (-(d + 1))) ⋯
P : K⸨X⸩ × K⸨X⸩
hP : P ∈ {P | Valued.v (P.2 - P.1) < ↑γ}
⊢ (P.1.coeff d, P.2.coeff d) ∈ S

Proof state:
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
⊢ UniformContinuous fun f => f.coeff d

Tactic:
refine uniformContinuous_iff_eventually.mpr fun S hS ↦ eventually_iff_exists_mem.mpr ?_

Result:
K : Type u_2
inst✝ : Field K
uK : UniformSpace K
d : ℤ
S : Set (K × K)
hS : S ∈ uniformity K
⊢ ∃ v ∈ uniformity K⸨X⸩, ∀ y ∈ v, (y.1.coeff d, y.2.coeff d) ∈ S