K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ ContinuousAt hatInv x
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ ContinuousAt hatInv x
haveI : T3Space (hat K) := Completion.t3Space K
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ ∀ᶠ (x : hat K) in 𝓝 x, ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ ContinuousAt hatInv x
refine' denseInducing_coe.continuousAt_extend _
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ {0}ᶜ ⊆ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ ∀ᶠ (x : hat K) in 𝓝 x, ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)
apply mem_of_superset (compl_singleton_mem_nhds h)
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ∈ {0}ᶜ
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
⊢ {0}ᶜ ⊆ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
intro y y_ne
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ∈ {0}ᶜ
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
rw [mem_compl_singleton_iff] at y_ne
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ Cauchy (map (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 y)))
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 x)) (𝓝 c)) x}
apply CompleteSpace.complete
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 y)))
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ Cauchy (map (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 y)))
have : (fun (x : K) => (↑x⁻¹: hat K)) =
    ((fun (y : K) => (↑y: hat K))∘(fun (x : K) => (x⁻¹ : K))) := by
  unfold Function.comp
  simp
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun y => ↑K y) (map (fun x => x⁻¹) (Filter.comap (↑K) (𝓝 y))))
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => ↑K x⁻¹) (Filter.comap (↑K) (𝓝 y)))
rw [this, ← Filter.map_map]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => x⁻¹) (Filter.comap (↑K) (𝓝 y)))
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun y => ↑K y) (map (fun x => x⁻¹) (Filter.comap (↑K) (𝓝 y))))
apply Cauchy.map _ (Completion.uniformContinuous_coe K)
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (Filter.comap (↑K) (𝓝 y))

case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap (↑K) (𝓝 y) = ⊥
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => x⁻¹) (Filter.comap (↑K) (𝓝 y)))
apply CompletableTopField.nice
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ (fun x => ↑K x⁻¹) = fun x => (fun y => ↑K y) ((fun x => x⁻¹) x)
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
unfold Function.comp
no goals
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
⊢ (fun x => ↑K x⁻¹) = fun x => (fun y => ↑K y) ((fun x => x⁻¹) x)
simp
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝¹ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
this : NeBot (Filter.comap (↑K) (𝓝 y))
⊢ Cauchy (Filter.comap (↑K) (𝓝 y))
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ Cauchy (Filter.comap (↑K) (𝓝 y))
haveI := denseInducing_coe.comap_nhds_neBot y
case a.hm
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝¹ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
this : NeBot (Filter.comap (↑K) (𝓝 y))
⊢ Filter.comap (fun p => (↑K p.fst, ↑K p.snd)) (uniformity (hat K)) ≤ uniformity K
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝¹ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
this : NeBot (Filter.comap (↑K) (𝓝 y))
⊢ Cauchy (Filter.comap (↑K) (𝓝 y))
apply cauchy_nhds.comap
no goals
case a.hm
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝¹ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
this : NeBot (Filter.comap (↑K) (𝓝 y))
⊢ Filter.comap (fun p => (↑K p.fst, ↑K p.snd)) (uniformity (hat K)) ≤ uniformity K
rw [Completion.comap_coe_eq_uniformity]
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ 𝓝 0 ⊓ Filter.comap (↑K) (𝓝 y) = ⊥
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap (↑K) (𝓝 y) = ⊥
have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
  by_contra h
  exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap ↑K ⊥ = ⊥
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ 𝓝 0 ⊓ Filter.comap (↑K) (𝓝 y) = ⊥
erw [denseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf, eq_bot]
no goals
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap ↑K ⊥ = ⊥
exact comap_bot
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h✝ : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
h : ¬𝓝 0 ⊓ 𝓝 y = ⊥
⊢ False
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
⊢ 𝓝 0 ⊓ 𝓝 y = ⊥
by_contra h
no goals
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h✝ : x ≠ 0
this✝ : T3Space (hat K)
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑K x⁻¹) = (fun y => ↑K y) ∘ fun x => x⁻¹
h : ¬𝓝 0 ⊓ 𝓝 y = ⊥
⊢ False
exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm