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

Tactic:
refine Set.Subset.trans (fun a _ ↦ ?_) (Set.preimage_mono γ_le)

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

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 : Set ℤₘ₀
hS : S ∈ 𝓝 (Valued.v a)
⊢ ψ ⁻¹' S ∈ comap UniformSpace.Completion.coe' (𝓝 a)

Tactic:
rw [ha, map_zero, WithZeroTopology.hasBasis_nhds_zero.1 S] at 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 : ∃ i, i ≠ 0 ∧ Set.Iio i ⊆ S
⊢ ψ ⁻¹' S ∈ comap UniformSpace.Completion.coe' (𝓝 a)

Proof state:
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))

Tactic:
have := Valued.is_topological_valuation (R := (idealX K).adicCompletion (RatFunc K))

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
⊢ Tendsto ψ (comap UniformSpace.Completion.coe' (𝓝 a)) (𝓝 (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)
⊢ ∃ γ, {y | Valued.v (y - a) < ↑γ} ⊆ {x | ∀ (a_1 : RatFunc K), ↑a_1 = x → Valued.v a_1 = Valued.v a}

Tactic:
have γ_ne_zero : γ ≠ 0 := by
  rw [ne_eq, _root_.div_eq_zero_iff, Valuation.zero_iff]
  simpa only [coe_ne_zero, or_false]

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)
γ_ne_zero : γ ≠ 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.intro.intro
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
⊢ ψ ⁻¹' S ∈ comap UniformSpace.Completion.coe' (𝓝 a)

Tactic:
use {t | Valued.v t < γ}

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
⊢ {t | Valued.v t < γ} ∈ 𝓝 a ∧ UniformSpace.Completion.coe' ⁻¹' {t | Valued.v t < γ} ⊆ ψ ⁻¹' S

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
⊢ {x | Valued.v x < ↑(Units.mk0 γ γ_ne_zero)} ⊆ {t | Valued.v t < γ}

Tactic:
rw [Units.val_mk0]

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

Tactic:
intro y val_y b 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)
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

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

Tactic:
congr

Result:
no goals

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 : Set ℤₘ₀
hS : ∃ i, i ≠ 0 ∧ Set.Iio i ⊆ S
⊢ ψ ⁻¹' S ∈ comap UniformSpace.Completion.coe' (𝓝 a)

Tactic:
obtain ⟨γ, γ_ne_zero, γ_le⟩ := hS

Result:
case pos.intro.intro
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
⊢ ψ ⁻¹' S ∈ comap UniformSpace.Completion.coe' (𝓝 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)
⊢ ¬(a = 0 ∨ ↑(Multiplicative.ofAdd 1) = 0)

Tactic:
simpa only [coe_ne_zero, or_false]

Result:
no goals