-- Mathlib/Topology/Algebra/UniformField.lean
theorem continuous_hatInv [CompletableTopField K] {x : hat K} (h : x ≠ 0) :
    ContinuousAt hatInv x

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ ∀ᶠ (x : hat K) in 𝓝 x, ∃ c, Tendsto (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)

Tactic:
apply mem_of_superset (compl_singleton_mem_nhds h)

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ {0}ᶜ ⊆ {x | (fun x => ∃ c, Tendsto (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h✝ : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
h : ¬𝓝 0 ⊓ 𝓝 y = ⊥
⊢ False

Tactic:
exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm

Result:
no goals

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
erw [isDenseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf, eq_bot]

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' ⊥ = ⊥

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
this : (Filter.comap coe' (𝓝 y)).NeBot
⊢ Cauchy (Filter.comap coe' (𝓝 y))

Tactic:
apply cauchy_nhds.comap

Result:
case a.hm
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
this : (Filter.comap coe' (𝓝 y)).NeBot
⊢ Filter.comap (fun p => (↑p.1, ↑p.2)) (uniformity (hat K)) ≤ uniformity K

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 y)))

Tactic:
rw [this, ← Filter.map_map]

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun y => ↑y) (map (fun x => x⁻¹) (Filter.comap coe' (𝓝 y))))

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ Cauchy (map (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 y)))

Tactic:
have : (fun (x : K) => (↑x⁻¹ : hat K)) =
    ((fun (y : K) => (↑y : hat K))∘(fun (x : K) => (x⁻¹ : K))) := by
  unfold Function.comp
  simp

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 y)))

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹

Tactic:
unfold Function.comp

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ (fun x => ↑x⁻¹) = fun x => (fun y => ↑y) ((fun x => x⁻¹) x)

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Filter.comap coe' ⊥ = ⊥

Tactic:
exact comap_bot

Result:
no goals

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => x⁻¹) (Filter.comap coe' (𝓝 y)))

Tactic:
apply CompletableTopField.nice

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ Cauchy (Filter.comap coe' (𝓝 y))

case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun y => ↑y) (map (fun x => x⁻¹) (Filter.comap coe' (𝓝 y))))

Tactic:
apply Cauchy.map _ (Completion.uniformContinuous_coe K)

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ Cauchy (map (fun x => x⁻¹) (Filter.comap coe' (𝓝 y)))

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ∈ {0}ᶜ
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}

Tactic:
rw [mem_compl_singleton_iff] at y_ne

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}

Tactic:
apply CompleteSpace.complete

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ Cauchy (map (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 y)))

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ Cauchy (Filter.comap coe' (𝓝 y))

Tactic:
haveI := isDenseInducing_coe.comap_nhds_neBot y

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
this : (Filter.comap coe' (𝓝 y)).NeBot
⊢ Cauchy (Filter.comap coe' (𝓝 y))

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ {0}ᶜ ⊆ {x | (fun x => ∃ c, Tendsto (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}

Tactic:
intro y y_ne

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ∈ {0}ᶜ
⊢ y ∈ {x | (fun x => ∃ c, Tendsto (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ 𝓝 0 ⊓ 𝓝 y = ⊥

Tactic:
by_contra h

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h✝ : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
h : ¬𝓝 0 ⊓ 𝓝 y = ⊥
⊢ False