[GOAL]
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ ContinuousAt hatInv x
[PROOFSTEP]
haveI : T3Space (hat K) := Completion.t3Space K
[GOAL]
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
[PROOFSTEP]
refine' denseInducing_coe.continuousAt_extend _
[GOAL]
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)
[PROOFSTEP]
apply mem_of_superset (compl_singleton_mem_nhds h)
[GOAL]
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}
[PROOFSTEP]
intro y y_ne
[GOAL]
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}
[PROOFSTEP]
rw [mem_compl_singleton_iff] at y_ne 
[GOAL]
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}
[PROOFSTEP]
apply CompleteSpace.complete
[GOAL]
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)))
[PROOFSTEP]
have : (fun (x : K) => (↑x⁻¹ : hat K)) = ((fun (y : K) => (↑y : hat K)) ∘ (fun (x : K) => (x⁻¹ : K))) :=
  by
  unfold Function.comp
  simp
[GOAL]
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⁻¹
[PROOFSTEP]
unfold Function.comp
[GOAL]
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)
[PROOFSTEP]
simp
[GOAL]
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)))
[PROOFSTEP]
rw [this, ← Filter.map_map]
[GOAL]
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))))
[PROOFSTEP]
apply Cauchy.map _ (Completion.uniformContinuous_coe K)
[GOAL]
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)))
[PROOFSTEP]
apply CompletableTopField.nice
[GOAL]
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))
[PROOFSTEP]
haveI := denseInducing_coe.comap_nhds_neBot y
[GOAL]
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))
[PROOFSTEP]
apply cauchy_nhds.comap
[GOAL]
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
[PROOFSTEP]
rw [Completion.comap_coe_eq_uniformity]
[GOAL]
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) = ⊥
[PROOFSTEP]
have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
  by_contra h
  exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
[GOAL]
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 = ⊥
[PROOFSTEP]
by_contra h
[GOAL]
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
[PROOFSTEP]
exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
[GOAL]
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) = ⊥
[PROOFSTEP]
erw [denseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf, eq_bot]
[GOAL]
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 ⊥ = ⊥
[PROOFSTEP]
exact comap_bot
[GOAL]
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
⊢ (↑K x)⁻¹ = ↑K x⁻¹
[PROOFSTEP]
by_cases h : x = 0
[GOAL]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑K x)⁻¹ = ↑K x⁻¹
[PROOFSTEP]
rw [h, inv_zero]
[GOAL]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (↑K 0)⁻¹ = ↑K 0
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if ↑K 0 = 0 then 0 else hatInv (↑K 0)) = ↑K 0
[PROOFSTEP]
norm_cast
[GOAL]
case pos
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : x = 0
⊢ (if 0 = 0 then 0 else hatInv 0) = 0
[PROOFSTEP]
simp
[GOAL]
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (↑K x)⁻¹ = ↑K x⁻¹
[PROOFSTEP]
conv_lhs => dsimp [Inv.inv]
[GOAL]
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
| (↑K x)⁻¹
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
| (↑K x)⁻¹
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
| (↑K x)⁻¹
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ (if ↑K x = 0 then 0 else hatInv (↑K x)) = ↑K x⁻¹
[PROOFSTEP]
rw [if_neg]
[GOAL]
case neg
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ hatInv (↑K x) = ↑K x⁻¹
[PROOFSTEP]
exact hatInv_extends h
[GOAL]
case neg.hnc
K : Type u_1
inst✝³ : Field K
inst✝² : UniformSpace K
inst✝¹ : TopologicalDivisionRing K
inst✝ : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬↑K x = 0
[PROOFSTEP]
exact fun H => h (denseEmbedding_coe.inj H)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ x * hatInv x = 1
[PROOFSTEP]
haveI : T1Space (hat K) := T2Space.t1Space
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
⊢ x * hatInv x = 1
[PROOFSTEP]
let f := fun x : hat K => x * hatInv x
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
⊢ x * hatInv x = 1
[PROOFSTEP]
let c := (fun (x : K) => (x : hat K))
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
⊢ x * hatInv x = 1
[PROOFSTEP]
change f x = 1
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
⊢ f x = 1
[PROOFSTEP]
have cont : ContinuousAt f x :=
  by
  letI : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
  have : ContinuousAt (fun y : hat K => ((y, hatInv y) : hat K × hat K)) x :=
    continuous_id.continuousAt.prod (continuous_hatInv x_ne)
  exact (_root_.continuous_mul.continuousAt.comp this : _)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
⊢ ContinuousAt f x
[PROOFSTEP]
letI : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
this : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
⊢ ContinuousAt f x
[PROOFSTEP]
have : ContinuousAt (fun y : hat K => ((y, hatInv y) : hat K × hat K)) x :=
  continuous_id.continuousAt.prod (continuous_hatInv x_ne)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝¹ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
this✝ : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
this : ContinuousAt (fun y => (y, hatInv y)) x
⊢ ContinuousAt f x
[PROOFSTEP]
exact (_root_.continuous_mul.continuousAt.comp this : _)
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
⊢ f x = 1
[PROOFSTEP]
have clo : x ∈ closure (c '' {0}ᶜ) := by
  have := denseInducing_coe.dense x
  rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm, image_union] at this 
  apply mem_closure_of_mem_closure_union this
  rw [image_singleton]
  exact compl_singleton_mem_nhds x_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
⊢ x ∈ closure (c '' {0}ᶜ)
[PROOFSTEP]
have := denseInducing_coe.dense x
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
this : x ∈ closure (range ↑K)
⊢ x ∈ closure (c '' {0}ᶜ)
[PROOFSTEP]
rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm, image_union] at this 
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
this : x ∈ closure (↑K '' {0} ∪ ↑K '' {0}ᶜ)
⊢ x ∈ closure (c '' {0}ᶜ)
[PROOFSTEP]
apply mem_closure_of_mem_closure_union this
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
this : x ∈ closure (↑K '' {0} ∪ ↑K '' {0}ᶜ)
⊢ (↑K '' {0})ᶜ ∈ 𝓝 x
[PROOFSTEP]
rw [image_singleton]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
this : x ∈ closure (↑K '' {0} ∪ ↑K '' {0}ᶜ)
⊢ {↑K 0}ᶜ ∈ 𝓝 x
[PROOFSTEP]
exact compl_singleton_mem_nhds x_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
⊢ f x = 1
[PROOFSTEP]
have fxclo : f x ∈ closure (f '' (c '' {0}ᶜ)) := mem_closure_image cont clo
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ f x = 1
[PROOFSTEP]
have : f '' (c '' {0}ᶜ) ⊆ {1} := by
  rw [image_image]
  rintro _ ⟨z, z_ne, rfl⟩
  rw [mem_singleton_iff]
  rw [mem_compl_singleton_iff] at z_ne 
  dsimp
  rw [hatInv_extends z_ne, ← coe_mul]
  rw [mul_inv_cancel z_ne, coe_one]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ f '' (c '' {0}ᶜ) ⊆ {1}
[PROOFSTEP]
rw [image_image]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ (fun x => f (c x)) '' {0}ᶜ ⊆ {1}
[PROOFSTEP]
rintro _ ⟨z, z_ne, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ∈ {0}ᶜ
⊢ (fun x => f (c x)) z ∈ {1}
[PROOFSTEP]
rw [mem_singleton_iff]
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ∈ {0}ᶜ
⊢ (fun x => f (c x)) z = 1
[PROOFSTEP]
rw [mem_compl_singleton_iff] at z_ne 
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ (fun x => f (c x)) z = 1
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ ↑K z * hatInv (↑K z) = 1
[PROOFSTEP]
rw [hatInv_extends z_ne, ← coe_mul]
[GOAL]
case intro.intro
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ ↑K (z * z⁻¹) = 1
[PROOFSTEP]
rw [mul_inv_cancel z_ne, coe_one]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
this : f '' (c '' {0}ᶜ) ⊆ {1}
⊢ f x = 1
[PROOFSTEP]
replace fxclo := closure_mono this fxclo
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
x : hat K
x_ne : x ≠ 0
this✝ : T1Space (hat K)
f : hat K → hat K := fun x => x * hatInv x
c : K → hat K := fun x => ↑K x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
this : f '' (c '' {0}ᶜ) ⊆ {1}
fxclo : f x ∈ closure {1}
⊢ f x = 1
[PROOFSTEP]
rwa [closure_singleton, mem_singleton_iff] at fxclo 
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : Inv (hat K) := instInvCompletion
⊢ CommRing (hat K)
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝¹ : Inv (hat K) := instInvCompletion
src✝ : CommRing (hat K) := inferInstance
x : hat K
x_ne : x ≠ 0
⊢ x * x⁻¹ = 1
[PROOFSTEP]
simp only [Inv.inv, if_neg x_ne, mul_hatInv_cancel x_ne]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝¹ : Inv (hat K) := instInvCompletion
src✝ : CommRing (hat K) := inferInstance
⊢ 0⁻¹ = 0
[PROOFSTEP]
simp only [Inv.inv, ite_true]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
⊢ ∀ ⦃x : hat K⦄, x ≠ 0 → ContinuousAt Inv.inv x
[PROOFSTEP]
intro x x_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
⊢ ContinuousAt Inv.inv x
[PROOFSTEP]
have : {y | hatInv y = y⁻¹} ∈ 𝓝 x :=
  haveI : {(0 : hat K)}ᶜ ⊆ {y : hat K | hatInv y = y⁻¹} :=
    by
    intro y y_ne
    rw [mem_compl_singleton_iff] at y_ne 
    dsimp [Inv.inv]
    rw [if_neg y_ne]
  mem_of_superset (compl_singleton_mem_nhds x_ne) this
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
⊢ {0}ᶜ ⊆ {y | hatInv y = y⁻¹}
[PROOFSTEP]
intro y y_ne
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ∈ {0}ᶜ
⊢ y ∈ {y | hatInv y = y⁻¹}
[PROOFSTEP]
rw [mem_compl_singleton_iff] at y_ne 
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {y | hatInv y = y⁻¹}
[PROOFSTEP]
dsimp [Inv.inv]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ hatInv y = if y = 0 then 0 else hatInv y
[PROOFSTEP]
rw [if_neg y_ne]
[GOAL]
K : Type u_1
inst✝⁴ : Field K
inst✝³ : UniformSpace K
inst✝² : TopologicalDivisionRing K
inst✝¹ : CompletableTopField K
inst✝ : UniformAddGroup K
src✝ : TopologicalRing (hat K) := topologicalRing
x : hat K
x_ne : x ≠ 0
this : {y | hatInv y = y⁻¹} ∈ 𝓝 x
⊢ ContinuousAt Inv.inv x
[PROOFSTEP]
exact ContinuousAt.congr (continuous_hatInv x_ne) this
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
⊢ ∀ (F : Filter { x // x ∈ K }), Cauchy F → 𝓝 0 ⊓ F = ⊥ → Cauchy (Filter.map (fun x => x⁻¹) F)
[PROOFSTEP]
intro F F_cau inf_F
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (Filter.map (fun x => x⁻¹) F)
[PROOFSTEP]
let i : K →+* L := K.subtype
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
⊢ Cauchy (Filter.map (fun x => x⁻¹) F)
[PROOFSTEP]
have hi : UniformInducing i := uniformEmbedding_subtype_val.toUniformInducing
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
hi : UniformInducing ↑i
⊢ Cauchy (Filter.map (fun x => x⁻¹) F)
[PROOFSTEP]
rw [← hi.cauchy_map_iff] at F_cau ⊢
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
⊢ Cauchy (Filter.map (↑i) (Filter.map (fun x => x⁻¹) F))
[PROOFSTEP]
rw [map_comm (show (i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ i by ext; rfl)]
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
⊢ (↑i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ↑i
[PROOFSTEP]
ext
[GOAL]
case h
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
x✝ : { x // x ∈ K }
⊢ (↑i ∘ fun x => x⁻¹) x✝ = ((fun x => x⁻¹) ∘ ↑i) x✝
[PROOFSTEP]
rfl
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
⊢ Cauchy (Filter.map (fun x => x⁻¹) (Filter.map (↑i) F))
[PROOFSTEP]
apply CompletableTopField.nice _ F_cau
[GOAL]
K✝ : Type u_1
inst✝⁴ : Field K✝
inst✝³ : UniformSpace K✝
L : Type u_2
inst✝² : Field L
inst✝¹ : UniformSpace L
inst✝ : CompletableTopField L
K : Subfield L
src✝ : SeparatedSpace ↑↑K := Subtype.separatedSpace ↑K
F : Filter { x // x ∈ K }
inf_F : 𝓝 0 ⊓ F = ⊥
i : { x // x ∈ K } →+* L := subtype K
F_cau : Cauchy (Filter.map (↑i) F)
hi : UniformInducing ↑i
⊢ 𝓝 0 ⊓ Filter.map (↑i) F = ⊥
[PROOFSTEP]
rw [← Filter.push_pull', ← map_zero i, ← hi.inducing.nhds_eq_comap, inf_F, Filter.map_bot]
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (fun x => x⁻¹) F)
[PROOFSTEP]
haveI : NeBot F := cau_F.1
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
⊢ Cauchy (map (fun x => x⁻¹) F)
[PROOFSTEP]
rcases CompleteSpace.complete cau_F with ⟨x, hx⟩
[GOAL]
case intro
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
x : L
hx : F ≤ 𝓝 x
⊢ Cauchy (map (fun x => x⁻¹) F)
[PROOFSTEP]
have hx' : x ≠ 0 := by
  rintro rfl
  rw [inf_eq_right.mpr hx] at hF 
  exact cau_F.1.ne hF
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
x : L
hx : F ≤ 𝓝 x
⊢ x ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
hx : F ≤ 𝓝 0
⊢ False
[PROOFSTEP]
rw [inf_eq_right.mpr hx] at hF 
[GOAL]
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : F = ⊥
this : NeBot F
hx : F ≤ 𝓝 0
⊢ False
[PROOFSTEP]
exact cau_F.1.ne hF
[GOAL]
case intro
K : Type u_1
inst✝⁹ : Field K
inst✝⁸ : UniformSpace K
L✝ : Type u_2
inst✝⁷ : Field L✝
inst✝⁶ : UniformSpace L✝
inst✝⁵ : CompletableTopField L✝
L : Type u_3
inst✝⁴ : Field L
inst✝³ : UniformSpace L
inst✝² : TopologicalDivisionRing L
inst✝¹ : SeparatedSpace L
inst✝ : CompleteSpace L
src✝ : SeparatedSpace L := inst✝¹
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : NeBot F
x : L
hx : F ≤ 𝓝 x
hx' : x ≠ 0
⊢ Cauchy (map (fun x => x⁻¹) F)
[PROOFSTEP]
exact
  Filter.Tendsto.cauchy_map
    (calc
      map (fun x => x⁻¹) F ≤ map (fun x => x⁻¹) (𝓝 x) := map_mono hx
      _ ≤ 𝓝 x⁻¹ := continuousAt_inv₀ hx')
