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
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
haveI : T1Space (hat K) := T2Space.t1Space
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
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
let f := fun x : hat K => x * hatInv x
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
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
let c := (fun (x : K) => (x : hat K))
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
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
change f x = 1
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
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
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 : _)
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
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
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
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
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
have fxclo : f x ∈ closure (f '' (c '' {0}ᶜ)) := mem_closure_image cont clo
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
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
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]
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
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
replace fxclo := closure_mono this fxclo
no goals
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
rwa [closure_singleton, mem_singleton_iff] at fxclo
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
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
letI : TopologicalSpace (hat K × hat K) := instTopologicalSpaceProd
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
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
have : ContinuousAt (fun y : hat K => ((y, hatInv y) : hat K × hat K)) x :=
  continuous_id.continuousAt.prod (continuous_hatInv x_ne)
no goals
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
exact (_root_.continuous_mul.continuousAt.comp this : _)
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}ᶜ)
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}ᶜ)
have := denseInducing_coe.dense x
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}ᶜ)
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}ᶜ)
rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm,
  image_union] at this
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
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}ᶜ)
apply mem_closure_of_mem_closure_union this
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
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
rw [image_singleton]
no goals
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
exact compl_singleton_mem_nhds x_ne
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}
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}
rw [image_image]
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}
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}
rintro _ ⟨z, z_ne, rfl⟩
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
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}
rw [mem_singleton_iff]
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
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
rw [mem_compl_singleton_iff] at z_ne
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
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
dsimp
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
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
rw [hatInv_extends z_ne, ← coe_mul]
no goals
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
rw [mul_inv_cancel z_ne, coe_one]