-- Mathlib/RingTheory/LaurentSeries.lean
theorem tendsto_valuation (a : (idealX K).adicCompletion (RatFunc K)) :
    Tendsto (Valued.v : RatFunc K → ℤₘ₀) (comap (↑) (𝓝 a)) (𝓝 (Valued.v a : ℤₘ₀))

Proof state:
case h.left
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
S : Set ℤₘ₀
γ : ℤₘ₀
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ {t | Valued.v t < γ} ∈ 𝓝 a

Tactic:
rw [ha, this]

Result:
case h.left
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
S : Set ℤₘ₀
γ : ℤₘ₀
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ ∃ γ_1, {x | Valued.v x < ↑γ_1} ⊆ {t | Valued.v t < γ}

Proof state:
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : ¬a = 0
γ : ℤₘ₀ := Valued.v a / ↑(Multiplicative.ofAdd 1)
h_aγ : γ = Valued.v a / ↑(Multiplicative.ofAdd 1)
γ_ne_zero : γ ≠ 0
y : adicCompletion (RatFunc K) (idealX K)
val_y : y ∈ {y | Valued.v (y - a) < ↑(Units.mk0 γ γ_ne_zero)}
b : RatFunc K
diff_b_y : ↑b = y
⊢ ↑(Units.mk0 γ γ_ne_zero) < Valued.v a

Tactic:
rw [Units.val_mk0, h_aγ, ← coe_unzero ((Valuation.ne_zero_iff Valued.v).mpr ha), ←
  WithZero.coe_div, coe_lt_coe, div_lt_self_iff, ← ofAdd_zero,
  Multiplicative.ofAdd_lt]

Result:
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : ¬a = 0
γ : ℤₘ₀ := Valued.v a / ↑(Multiplicative.ofAdd 1)
h_aγ : γ = Valued.v a / ↑(Multiplicative.ofAdd 1)
γ_ne_zero : γ ≠ 0
y : adicCompletion (RatFunc K) (idealX K)
val_y : y ∈ {y | Valued.v (y - a) < ↑(Units.mk0 γ γ_ne_zero)}
b : RatFunc K
diff_b_y : ↑b = y
⊢ 0 < 1

Proof state:
case h
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : ¬a = 0
γ : ℤₘ₀ := Valued.v a / ↑(Multiplicative.ofAdd 1)
h_aγ : γ = Valued.v a / ↑(Multiplicative.ofAdd 1)
γ_ne_zero : γ ≠ 0
y : adicCompletion (RatFunc K) (idealX K)
val_y : y ∈ {y | Valued.v (y - a) < ↑(Units.mk0 γ γ_ne_zero)}
b : RatFunc K
diff_b_y : ↑b = y
⊢ Valued.v b = Valued.v a

Tactic:
replace val_y : Valued.v y = Valued.v a := by
  refine Valuation.map_eq_of_sub_lt _ (val_y.trans ?_)
  rw [Units.val_mk0, h_aγ, ← coe_unzero ((Valuation.ne_zero_iff Valued.v).mpr ha), ←
    WithZero.coe_div, coe_lt_coe, div_lt_self_iff, ← ofAdd_zero,
    Multiplicative.ofAdd_lt]
  exact Int.zero_lt_one

Result:
case h
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : ¬a = 0
γ : ℤₘ₀ := Valued.v a / ↑(Multiplicative.ofAdd 1)
h_aγ : γ = Valued.v a / ↑(Multiplicative.ofAdd 1)
γ_ne_zero : γ ≠ 0
y : adicCompletion (RatFunc K) (idealX K)
b : RatFunc K
diff_b_y : ↑b = y
val_y : Valued.v y = Valued.v a
⊢ Valued.v b = Valued.v a

Proof state:
case neg
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : ¬a = 0
γ : ℤₘ₀ := Valued.v a / ↑(Multiplicative.ofAdd 1)
h_aγ : γ = Valued.v a / ↑(Multiplicative.ofAdd 1)
γ_ne_zero : γ ≠ 0
⊢ ∃ γ, {y | Valued.v (y - a) < ↑γ} ⊆ {x | ∀ (a_1 : RatFunc K), ↑a_1 = x → Valued.v a_1 = Valued.v a}

Tactic:
use Units.mk0 γ γ_ne_zero

Result:
case h
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : ¬a = 0
γ : ℤₘ₀ := Valued.v a / ↑(Multiplicative.ofAdd 1)
h_aγ : γ = Valued.v a / ↑(Multiplicative.ofAdd 1)
γ_ne_zero : γ ≠ 0
⊢ {y | Valued.v (y - a) < ↑(Units.mk0 γ γ_ne_zero)} ⊆ {x | ∀ (a_1 : RatFunc K), ↑a_1 = x → Valued.v a_1 = Valued.v a}

Proof state:
case h
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
S : Set ℤₘ₀
γ : ℤₘ₀
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ {t | Valued.v t < γ} ∈ 𝓝 a ∧ UniformSpace.Completion.coe' ⁻¹' {t | Valued.v t < γ} ⊆ ψ ⁻¹' S

Tactic:
constructor

Result:
case h.left
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
S : Set ℤₘ₀
γ : ℤₘ₀
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ {t | Valued.v t < γ} ∈ 𝓝 a

case h.right
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
S : Set ℤₘ₀
γ : ℤₘ₀
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ UniformSpace.Completion.coe' ⁻¹' {t | Valued.v t < γ} ⊆ ψ ⁻¹' S

Proof state:
case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
⊢ Tendsto ψ (comap UniformSpace.Completion.coe' (𝓝 a)) (𝓝 (Valued.v a))

Tactic:
rw [tendsto_def]

Result:
case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
⊢ ∀ s ∈ 𝓝 (Valued.v a), ψ ⁻¹' s ∈ comap UniformSpace.Completion.coe' (𝓝 a)

Proof state:
case neg
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : ¬a = 0
⊢ Tendsto ψ (comap UniformSpace.Completion.coe' (𝓝 a)) (𝓝 (Valued.v a))

Tactic:
rw [WithZeroTopology.tendsto_of_ne_zero ((Valuation.ne_zero_iff Valued.v).mpr ha), hψ,
  Filter.eventually_comap, Filter.Eventually, Valued.mem_nhds]

Result:
case neg
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : ¬a = 0
⊢ ∃ γ, {y | Valued.v (y - a) < ↑γ} ⊆ {x | ∀ (a_1 : RatFunc K), ↑a_1 = x → Valued.v a_1 = Valued.v a}

Proof state:
case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
⊢ ∀ s ∈ 𝓝 (Valued.v a), ψ ⁻¹' s ∈ comap UniformSpace.Completion.coe' (𝓝 a)

Tactic:
intro S hS

Result:
case pos
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
this : ∀ (s : Set (adicCompletion (RatFunc K) (idealX K))), s ∈ 𝓝 0 ↔ ∃ γ, {x | Valued.v x < ↑γ} ⊆ s
ha : a = 0
S : Set ℤₘ₀
hS : S ∈ 𝓝 (Valued.v a)
⊢ ψ ⁻¹' S ∈ comap UniformSpace.Completion.coe' (𝓝 a)