-- 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:
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

Tactic:
exact Int.zero_lt_one

Result:
no goals

Proof state:
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
⊢ Tendsto (⇑Valued.v) (comap UniformSpace.Completion.coe' (𝓝 a)) (𝓝 (Valued.v a))

Tactic:
set ψ := (Valued.v : RatFunc K → ℤₘ₀) with hψ

Result:
K : Type u_2
inst✝ : Field K
a : adicCompletion (RatFunc K) (idealX K)
ψ : RatFunc K → ℤₘ₀ := ⇑Valued.v
hψ : ψ = ⇑Valued.v
⊢ Tendsto ψ (comap UniformSpace.Completion.coe' (𝓝 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
⊢ ∃ γ_1, {x | Valued.v x < ↑γ_1} ⊆ {t | Valued.v t < γ}

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
S : Set ℤₘ₀
γ : ℤₘ₀
γ_ne_zero : γ ≠ 0
γ_le : Set.Iio γ ⊆ S
⊢ {x | Valued.v x < ↑(Units.mk0 γ γ_ne_zero)} ⊆ {t | Valued.v t < γ}

Proof state:
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
a : RatFunc K
x✝ : a ∈ UniformSpace.Completion.coe' ⁻¹' {t | Valued.v t < γ}
⊢ a ∈ ψ ⁻¹' Set.Iio γ

Tactic:
rwa [Set.mem_preimage, Set.mem_Iio, hψ, ← Valued.valuedCompletion_apply a]

Result:
no goals

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)
b : RatFunc K
diff_b_y : ↑b = y
val_y : Valued.v y = Valued.v a
⊢ Valued.v b = Valued.v a

Tactic:
rw [← Valued.extension_extends, ← val_y, ← diff_b_y]

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.extension ↑b = Valued.v ↑b

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
⊢ Valued.v y = Valued.v a

Tactic:
refine Valuation.map_eq_of_sub_lt _ (val_y.trans ?_)

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
⊢ ↑(Units.mk0 γ γ_ne_zero) < Valued.v a

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)
⊢ γ ≠ 0

Tactic:
rw [ne_eq, _root_.div_eq_zero_iff, Valuation.zero_iff]

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)
⊢ ¬(a = 0 ∨ ↑(Multiplicative.ofAdd 1) = 0)

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
⊢ ∃ γ, {y | Valued.v (y - a) < ↑γ} ⊆ {x | ∀ (a_1 : RatFunc K), ↑a_1 = x → Valued.v a_1 = Valued.v a}

Tactic:
set γ := Valued.v a / (↑(Multiplicative.ofAdd (1 : ℤ)) : ℤₘ₀) with h_aγ

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
γ : ℤₘ₀ := Valued.v a / ↑(Multiplicative.ofAdd 1)
h_aγ : γ = Valued.v a / ↑(Multiplicative.ofAdd 1)
⊢ ∃ γ, {y | Valued.v (y - a) < ↑γ} ⊆ {x | ∀ (a_1 : RatFunc K), ↑a_1 = x → Valued.v a_1 = Valued.v a}

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
⊢ Tendsto ψ (comap UniformSpace.Completion.coe' (𝓝 a)) (𝓝 (Valued.v a))

Tactic:
by_cases ha : a = 0

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
⊢ Tendsto ψ (comap UniformSpace.Completion.coe' (𝓝 a)) (𝓝 (Valued.v a))

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))