-- Mathlib/Topology/Algebra/UniformField.lean
theorem mul_hatInv_cancel {x : hat K} (x_ne : x ≠ 0) : x * hatInv x = 1

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
this : x ∈ closure (range coe')
⊢ x ∈ closure (c '' {0}ᶜ)

Tactic:
rw [← image_univ, show (univ : Set K) = {0} ∪ {0}ᶜ from (union_compl_self _).symm,
  image_union] at this

Result:
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 * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
this : x ∈ closure (coe' '' {0} ∪ coe' '' {0}ᶜ)
⊢ x ∈ closure (c '' {0}ᶜ)

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑x
⊢ f x = 1

Tactic:
have cont : ContinuousAt f x := by
  fun_prop (disch := assumption)

Result:
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 * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
⊢ f x = 1

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ f '' (c '' {0}ᶜ) ⊆ {1}

Tactic:
rw [image_image]

Result:
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 * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ (fun x => f (c x)) '' {0}ᶜ ⊆ {1}

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑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}

Tactic:
rw [mem_singleton_iff]

Result:
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 * x.hatInv
c : K → hat K := fun x => ↑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

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
this : f '' (c '' {0}ᶜ) ⊆ {1}
fxclo : f x ∈ closure {1}
⊢ f x = 1

Tactic:
rwa [closure_singleton, mem_singleton_iff] at fxclo

Result:
no goals

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑x
⊢ ContinuousAt f x

Tactic:
fun_prop (disch := assumption)

Result:
no goals

Proof state:
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 * x.hatInv = 1

Tactic:
let f := fun x : hat K => x * hatInv x

Result:
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 * x.hatInv
⊢ x * x.hatInv = 1

Proof state:
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 * x.hatInv
⊢ x * x.hatInv = 1

Tactic:
let c := (fun (x : K) => (x : hat K))

Result:
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 * x.hatInv
c : K → hat K := fun x => ↑x
⊢ x * x.hatInv = 1

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
z : K
z_ne : z ≠ 0
⊢ ↑(z * z⁻¹) = 1

Tactic:
rw [mul_inv_cancel₀ z_ne, coe_one]

Result:
no goals

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑x
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' (c '' {0}ᶜ))
⊢ f x = 1

Tactic:
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 [f]
  rw [hatInv_extends z_ne, ← coe_mul]
  rw [mul_inv_cancel₀ z_ne, coe_one]

Result:
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 * x.hatInv
c : K → hat K := fun x => ↑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

Proof state:
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 * x.hatInv
c : K → hat K := fun x => ↑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

Tactic:
rw [mem_compl_singleton_iff] at z_ne

Result:
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 * x.hatInv
c : K → hat K := fun x => ↑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