-- Mathlib/Topology/Algebra/UniformField.lean
theorem IsUniformInducing.completableTopField
    [UniformSpace α] [T0Space α]
    {f : α →+* β} (hf : IsUniformInducing f) :
    CompletableTopField α

Proof state:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (⇑f) (map (fun x => x⁻¹) F))

Tactic:
have h_comm : (f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ f := by
  ext; simp only [Function.comp_apply, map_inv₀, Subfield.coe_inv]

Result:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ⇑f
⊢ Cauchy (map (⇑f) (map (fun x => x⁻¹) F))

Proof state:
case h
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
x✝ : α
⊢ (⇑f ∘ fun x => x⁻¹) x✝ = ((fun x => x⁻¹) ∘ ⇑f) x✝

Tactic:
simp only [Function.comp_apply, map_inv₀, Subfield.coe_inv]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ⇑f
⊢ Cauchy (map (fun x => x⁻¹) (map (⇑f) F))

Tactic:
apply CompletableTopField.nice _ F_cau

Result:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ⇑f
⊢ 𝓝 0 ⊓ map (⇑f) F = ⊥

Proof state:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
⊢ CompletableTopField α

Tactic:
refine CompletableTopField.mk (fun F F_cau inf_F => ?_)

Result:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (fun x => x⁻¹) F)

Proof state:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ⇑f
⊢ 𝓝 0 ⊓ map (⇑f) F = ⊥

Tactic:
rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ (⇑f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ⇑f

Tactic:
ext

Result:
case h
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
x✝ : α
⊢ (⇑f ∘ fun x => x⁻¹) x✝ = ((fun x => x⁻¹) ∘ ⇑f) x✝

Proof state:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ⇑f
⊢ Cauchy (map (⇑f) (map (fun x => x⁻¹) F))

Tactic:
rw [Filter.map_comm h_comm]

Result:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm : (⇑f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ ⇑f
⊢ Cauchy (map (fun x => x⁻¹) (map (⇑f) F))

Proof state:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (fun x => x⁻¹) F)

Tactic:
rw [← IsUniformInducing.cauchy_map_iff hf] at F_cau ⊢

Result:
α : Type u_3
β : Type u_4
inst✝⁴ : Field β
b : UniformSpace β
inst✝³ : CompletableTopField β
inst✝² : Field α
inst✝¹ : UniformSpace α
inst✝ : T0Space α
f : α →+* β
hf : IsUniformInducing ⇑f
F : Filter α
F_cau : Cauchy (map (⇑f) F)
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (map (⇑f) (map (fun x => x⁻¹) F))