awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬Eq (α := hat K) (↑x : hat K) 0

Tactic:
fun H => h (isDenseEmbedding_coe.injective H)

Premises used: Not, UniformSpace.Completion.isDenseEmbedding_coe, IsDenseEmbedding.injective
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
h : ¬x = 0
⊢ ¬Eq (α := hat K) (↑x : hat K) 0

Tactic:
exact fun H => h (isDenseEmbedding_coe.injective H)

Premises used: UniformSpace.Completion.isDenseEmbedding_coe, IsDenseEmbedding.injective
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ T1Space.{u_1} (hat K)

Tactic:
haveI : T1Space (hat K) := T2Space.t1Space
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
change : f x = 1
⊢ x * x.hatInv = 1

Tactic:
change f x = 1
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
funProp : x ≠ 0
⊢ ContinuousAt f x

Tactic:
fun_prop
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
⊢ ContinuousAt f x

Tactic:
have cont : ContinuousAt f x := by fun_prop
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
⊢ Membership.mem (γ := Set (hat K)) (closure (range coe')) x

Tactic:
have := isDenseInducing_coe.dense x
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this_1 : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
this : Membership.mem (γ := Set (hat K)) (closure (range coe')) x
⊢ Membership.mem (γ := Set (hat K)) (closure (coe' '' {0} ∪ coe' '' {0}ᶜ)) x

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

Premises used: Set.image_univ, Set.union_compl_self, Singleton.singleton, OfNat.ofNat, Eq.symm, Set.image_union
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this_1 : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
this : Membership.mem (γ := Set (hat K)) (closure (coe' '' {0} ∪ coe' '' {0}ᶜ)) x
apply : (coe' '' {0})ᶜ ∈ 𝓝 x
⊢ x ∈ closure (c '' {0}ᶜ)

Tactic:
apply mem_closure_of_mem_closure_union this

Premises used: mem_closure_of_mem_closure_union
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this_1 : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
this : Membership.mem (γ := Set (hat K)) (closure (coe' '' {0} ∪ coe' '' {0}ᶜ)) x
rw : {(↑0 : hat K)}ᶜ ∈ 𝓝 x
⊢ (coe' '' {0})ᶜ ∈ 𝓝 x

Tactic:
rw [image_singleton]

Premises used: Set.image_singleton
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this_1 : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
this : Membership.mem (γ := Set (hat K)) (closure (coe' '' {0} ∪ coe' '' {0}ᶜ)) x
⊢ {(↑0 : hat K)}ᶜ ∈ 𝓝 x

Tactic:
compl_singleton_mem_nhds x_ne

Premises used: compl_singleton_mem_nhds
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this_1 : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
this : Membership.mem (γ := Set (hat K)) (closure (coe' '' {0} ∪ coe' '' {0}ᶜ)) x
⊢ {(↑0 : hat K)}ᶜ ∈ 𝓝 x

Tactic:
exact compl_singleton_mem_nhds x_ne

Premises used: compl_singleton_mem_nhds
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
⊢ x ∈ closure (c '' {0}ᶜ)

Tactic:
have clo : x ∈ closure (c '' {0}ᶜ) := by
    have := isDenseInducing_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
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
⊢ f x ∈ closure (f '' c '' {0}ᶜ)

Tactic:
have fxclo : f x ∈ closure (f '' c '' {0}ᶜ) := mem_closure_image cont clo
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
rw : Subset (α := Set (hat K)) ((fun (x : K) ↦ f (c x)) '' {0}ᶜ) {1}
⊢ f '' c '' {0}ᶜ ⊆ {1}

Tactic:
rw [image_image]

Premises used: Set.image_image
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
z : K
z_ne : Membership.mem (γ := Set K) {0}ᶜ z
⊢ z ≠ 0

Tactic:
rw [mem_compl_singleton_iff] at z_ne

Premises used: Set.mem_compl_singleton_iff
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
z : K
z_ne : z ≠ 0
dsimp : c z * (c z).hatInv = 1
⊢ Eq.{u_1 + 1} (α := hat K) ((fun (x : K) ↦ f (c x)) z) 1

Tactic:
dsimp [f]
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
z : K
z_ne : z ≠ 0
rw : Eq (α := hat K) (↑(z * z⁻¹) : hat K) 1
⊢ c z * (c z).hatInv = 1

Tactic:
rw [hatInv_extends z_ne, ← coe_mul]

Premises used: UniformSpace.Completion.coe_mul, UniformSpace.Completion.hatInv_extends
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
z : K
z_ne : z ≠ 0
rw : Eq.{u_1 + 1} (α := hat K) (↑1 : hat K) 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := hat K) 1 1
⊢ Eq (α := hat K) (↑(z * z⁻¹) : hat K) 1

Tactic:
rw [mul_inv_cancel₀ z_ne, coe_one]

Premises used: mul_inv_cancel₀, UniformSpace.Completion.coe_one
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
⊢ f '' c '' {0}ᶜ ⊆ {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]
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this_1 : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
fxclo : f x ∈ closure (f '' c '' {0}ᶜ)
this : f '' c '' {0}ᶜ ⊆ {1}
⊢ Membership.mem (γ := Set (hat K)) (closure {1}) (f x)

Tactic:
replace fxclo := closure_mono this fxclo
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this_1 : T1Space.{u_1} (hat K)
f : (x : hat K) → hat K := fun (x : hat K) ↦ x * x.hatInv
c : (x : K) → hat K := fun (x : K) ↦ (↑x : hat K)
cont : ContinuousAt f x
clo : x ∈ closure (c '' {0}ᶜ)
this : f '' c '' {0}ᶜ ⊆ {1}
fxclo : Membership.mem (γ := Set (hat K)) (closure {1}) (f x)
rwa : ∀ (fxclo : Membership.mem (γ := Set (hat K)) {1} (f x)), f x = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (fxclo : f x = 1), f x = 1
⊢ f x = 1

Tactic:
rwa [closure_singleton, mem_singleton_iff] at fxclo

Premises used: closure_singleton, Set.mem_singleton_iff
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
simp only [Inv.inv, if_neg x_ne, mul_hatInv_cancel x_ne]

Premises used: UniformSpace.Completion.mul_hatInv_cancel, Inv.inv, if_neg
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
⊢ Eq.{u_1 + 1} (α := hat K) 0⁻¹ 0

Tactic:
simp only [Inv.inv, ite_true]

Premises used: ite_true, Inv.inv
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : Membership.mem (γ := Set (hat K)) {0}ᶜ y
⊢ y ≠ 0

Tactic:
rw [mem_compl_singleton_iff] at y_ne

Premises used: Set.mem_compl_singleton_iff
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
y : hat K
y_ne : y ≠ 0
rw rw₁ : y.hatInv = y.hatInv
⊢ y.hatInv = if y = 0 then 0 else y.hatInv

Tactic:
rw [if_neg y_ne]

Premises used: if_neg
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
⊢ {y : hat K | y.hatInv = y⁻¹} ∈ 𝓝 x

Tactic:
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
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : {y : hat K | y.hatInv = y⁻¹} ∈ 𝓝 x
⊢ ContinuousAt Inv.inv x

Tactic:
ContinuousAt.congr (continuous_hatInv x_ne) this

Premises used: UniformSpace.Completion.continuous_hatInv, ContinuousAt.congr
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
inst_4 : IsUniformAddGroup K
x : hat K
x_ne : x ≠ 0
this : {y : hat K | y.hatInv = y⁻¹} ∈ 𝓝 x
⊢ ContinuousAt Inv.inv x

Tactic:
exact ContinuousAt.congr (continuous_hatInv x_ne) this

Premises used: UniformSpace.Completion.continuous_hatInv, ContinuousAt.congr
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K_1 : Type u_1
inst : Field K_1
inst_1 : UniformSpace K_1
L : Type u_2
inst_2 : Field L
inst_3 : UniformSpace L
inst_4 : CompletableTopField L
K : Subfield L
F : Filter ↥K
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
⊢ IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)

Tactic:
have hi : IsUniformInducing i := isUniformEmbedding_subtype_val.isUniformInducing
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K_1 : Type u_1
inst : Field K_1
inst_1 : UniformSpace K_1
L : Type u_2
inst_2 : Field L
inst_3 : UniformSpace L
inst_4 : CompletableTopField L
K : Subfield L
F : Filter ↥K
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
hi : IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)
rw :
  ∀ (F_cau : Cauchy (α := L) (map (⇑i : (a : ↥K) → L) F))
    (hi : IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)),
    Cauchy (α := L) (map (α := ↥K) (⇑i : (a : ↥K) → L) (map (fun (x : ↥K) ↦ x⁻¹) F))
⊢ Cauchy (α := ↥K) (map (fun (x : ↥K) ↦ x⁻¹) F)

Tactic:
rw [← hi.cauchy_map_iff] at F_cau ⊢

Premises used: IsUniformInducing.cauchy_map_iff
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K_1 : Type u_1
inst : Field K_1
inst_1 : UniformSpace K_1
L : Type u_2
inst_2 : Field L
inst_3 : UniformSpace L
inst_4 : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (α := L) (map (⇑i : (a : ↥K) → L) F)
hi : IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)
h :
  ∀ (x : ↥K),
    Eq (α := L) (Function.comp (β := ↥K) (⇑i : (a : ↥K) → L) (fun (x : ↥K) ↦ x⁻¹) x)
      (((fun (x : L) ↦ x⁻¹) ∘ (⇑i : (a : ↥K) → L)) x)
⊢ Eq (α := ↥K → L) (Function.comp (β := ↥K) (⇑i : (a : ↥K) → L) fun (x : ↥K) ↦ x⁻¹)
    ((fun (x : L) ↦ x⁻¹) ∘ (⇑i : (a : ↥K) → L))

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K_1 : Type u_1
inst : Field K_1
inst_1 : UniformSpace K_1
L : Type u_2
inst_2 : Field L
inst_3 : UniformSpace L
inst_4 : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (α := L) (map (⇑i : (a : ↥K) → L) F)
hi : IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)
x : ↥K
⊢ Eq (α := L) (Function.comp (β := ↥K) (⇑i : (a : ↥K) → L) (fun (x : ↥K) ↦ x⁻¹) x)
    (((fun (x : L) ↦ x⁻¹) ∘ (⇑i : (a : ↥K) → L)) x)

Tactic:
rfl
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K_1 : Type u_1
inst : Field K_1
inst_1 : UniformSpace K_1
L : Type u_2
inst_2 : Field L
inst_3 : UniformSpace L
inst_4 : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (α := L) (map (⇑i : (a : ↥K) → L) F)
hi : IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)
rw : Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) (map (⇑i : (a : ↥K) → L) F))
⊢ Cauchy (α := L) (map (α := ↥K) (⇑i : (a : ↥K) → L) (map (fun (x : ↥K) ↦ x⁻¹) F))

Tactic:
rw [map_comm (show (i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ i by ext; rfl)]

Premises used: Filter.map_comm
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K_1 : Type u_1
inst : Field K_1
inst_1 : UniformSpace K_1
L : Type u_2
inst_2 : Field L
inst_3 : UniformSpace L
inst_4 : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (α := L) (map (⇑i : (a : ↥K) → L) F)
hi : IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)
apply : Eq (α := Filter L) (𝓝 0 ⊓ map (⇑i : (a : ↥K) → L) F) ⊥
⊢ Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) (map (⇑i : (a : ↥K) → L) F))

Tactic:
apply CompletableTopField.nice _ F_cau

Premises used: CompletableTopField.nice
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K_1 : Type u_1
inst : Field K_1
inst_1 : UniformSpace K_1
L : Type u_2
inst_2 : Field L
inst_3 : UniformSpace L
inst_4 : CompletableTopField L
K : Subfield L
F : Filter ↥K
inf_F : 𝓝 0 ⊓ F = ⊥
i : ↥K →+* L := K.subtype
F_cau : Cauchy (α := L) (map (⇑i : (a : ↥K) → L) F)
hi : IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)
rw : Eq (α := Filter L) (map (⇑i : (a : ↥K) → L) (Filter.comap (β := L) (⇑i : (a : ↥K) → L) (𝓝 0) ⊓ F)) ⊥
rw₁ :
  Eq (α := Filter L)
    (map (⇑i : (a : ↥K) → L)
      (Filter.comap (β := L) ((⇑i : (a : ↥K) → L) : (a : ↥K) → L) (𝓝 ((i : (a : ↥K) → L) 0) : Filter L) ⊓ F))
    ⊥
rw₂ : Eq (α := Filter L) (map (⇑i : (a : ↥K) → L) (𝓝 0 ⊓ F)) ⊥
rw₃ : Eq (α := Filter L) (map (α := ↥K) (⇑i : (a : ↥K) → L) ⊥) ⊥
rw₄ rw₅ : Eq.{u_2 + 1} (α := Filter L) ⊥ ⊥
⊢ Eq (α := Filter L) (𝓝 0 ⊓ map (⇑i : (a : ↥K) → L) F) ⊥

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

Premises used: Topology.IsInducing.nhds_eq_comap, Filter.map_bot, Filter.push_pull', map_zero, IsUniformInducing.isInducing
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
⊢ F.NeBot

Tactic:
haveI : NeBot F := cau_F.1
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
rcases : ∀ (x : L) (hx : F ≤ 𝓝 x), Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) F)
⊢ Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) F)

Tactic:
rcases CompleteSpace.complete cau_F with ⟨x, hx⟩

Premises used: CompleteSpace.complete
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
⊢ F = ⊥

Tactic:
rw [inf_eq_right.mpr hx] at hF

Premises used: Iff.mpr, inf_eq_right
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
hF₁ : F = ⊥
⊢ F.NeBot

Tactic:
rw [inf_eq_right.mpr hx] at hF

Premises used: Iff.mpr, inf_eq_right
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
hF₁ : F = ⊥
this₁ : F.NeBot
⊢ F ≤ 𝓝 0

Tactic:
rw [inf_eq_right.mpr hx] at hF

Premises used: Iff.mpr, inf_eq_right
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
⊢ False

Tactic:
cau_F.1.ne hF

Premises used: Filter.NeBot.ne, And.left
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : F = ⊥
this : F.NeBot
hx : F ≤ 𝓝 0
⊢ False

Tactic:
exact cau_F.1.ne hF

Premises used: Filter.NeBot.ne, And.left
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
L_1 : Type u_2
inst_2 : Field L_1
inst_3 : UniformSpace L_1
inst_4 : CompletableTopField L_1
L : Type u_3
inst_5 : Field L
inst_6 : UniformSpace L
inst_7 : IsTopologicalDivisionRing L
inst_8 : T0Space L
inst_9 : CompleteSpace L
F : Filter L
cau_F : Cauchy F
hF : 𝓝 0 ⊓ F = ⊥
this : F.NeBot
x : L
hx : F ≤ 𝓝 x
⊢ x ≠ 0

Tactic:
have hx' : x ≠ 0 := by
      rintro rfl
      rw [inf_eq_right.mpr hx] at hF
      exact cau_F.1.ne hF