awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (hypothesis)
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
⊢ Membership.mem (γ := Set (hat K)) {y : hat K | y.hatInv = y⁻¹} y
have y_ne₁ : y ≠ 0
Tactic: rw [mem_compl_singleton_iff] at y_ne
Cleared hypotheses: y_ne
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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
⊢ y.hatInv = if y = 0 then 0 else y.hatInv
have rw : y.hatInv = y.hatInv
Tactic: rw [if_neg y_ne]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (hypothesis)
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
⊢ ContinuousAt Inv.inv x
have this : {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
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (hypothesis)
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
⊢ Cauchy (α := ↥K) (map (fun (x : ↥K) ↦ x⁻¹) F)
have hi : IsUniformInducing (α := ↥K) (β := L) (⇑i : (a : ↥K) → L)
Tactic: have hi : IsUniformInducing i := isUniformEmbedding_subtype_val.isUniformInducing
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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)
⊢ Cauchy (α := ↥K) (map (fun (x : ↥K) ↦ x⁻¹) F)
have 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))
Tactic: rw [← hi.cauchy_map_iff] at F_cau ⊢
Cleared hypotheses: F_cau, hi
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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)
⊢ Eq (α := ↥K → L) (Function.comp (β := ↥K) (⇑i : (a : ↥K) → L) fun (x : ↥K) ↦ x⁻¹)
    ((fun (x : L) ↦ x⁻¹) ∘ (⇑i : (a : ↥K) → L))
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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)
⊢ Cauchy (α := L) (map (α := ↥K) (⇑i : (a : ↥K) → L) (map (fun (x : ↥K) ↦ x⁻¹) F))
have rw : Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) (map (⇑i : (a : ↥K) → L) F))
Tactic: rw [map_comm (show (i ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ i by ext; rfl)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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)
⊢ Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) (map (⇑i : (a : ↥K) → L) F))
have apply : Eq (α := Filter L) (𝓝 0 ⊓ map (⇑i : (a : ↥K) → L) F) ⊥
Tactic: apply CompletableTopField.nice _ F_cau
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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)
⊢ Eq (α := Filter L) (𝓝 0 ⊓ map (⇑i : (a : ↥K) → L) F) ⊥
have rw : Eq (α := Filter L) (map (⇑i : (a : ↥K) → L) (Filter.comap (β := L) (⇑i : (a : ↥K) → L) (𝓝 0) ⊓ F)) ⊥
Tactic: rw [← Filter.push_pull', ← map_zero i, ← hi.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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)) ⊥
⊢ Eq (α := Filter L) (𝓝 0 ⊓ map (⇑i : (a : ↥K) → L) F) ⊥
have 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))
  ⊥
Tactic: rw [← Filter.push_pull', ← map_zero i, ← hi.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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))
    ⊥
⊢ Eq (α := Filter L) (𝓝 0 ⊓ map (⇑i : (a : ↥K) → L) F) ⊥
have rw₂ : Eq (α := Filter L) (map (⇑i : (a : ↥K) → L) (𝓝 0 ⊓ F)) ⊥
Tactic: rw [← Filter.push_pull', ← map_zero i, ← hi.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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)) ⊥
⊢ Eq (α := Filter L) (𝓝 0 ⊓ map (⇑i : (a : ↥K) → L) F) ⊥
have rw₃ : Eq (α := Filter L) (map (α := ↥K) (⇑i : (a : ↥K) → L) ⊥) ⊥
Tactic: rw [← Filter.push_pull', ← map_zero i, ← hi.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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) ⊥) ⊥
⊢ Eq (α := Filter L) (𝓝 0 ⊓ map (⇑i : (a : ↥K) → L) F) ⊥
have rw₄ : Eq.{u_2 + 1} (α := Filter L) ⊥ ⊥
Tactic: rw [← Filter.push_pull', ← map_zero i, ← hi.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (hypothesis)
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 = ⊥
⊢ Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) F)
have this : F.NeBot
Tactic: haveI : NeBot F := cau_F.1
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
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
⊢ Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) F)
have rcases : ∀ (x : L) (hx : F ≤ 𝓝 x), Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) F)
Tactic: rcases CompleteSpace.complete cau_F with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (hypothesis)
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
⊢ False
have hF₁ : F = ⊥
Tactic: rw [inf_eq_right.mpr hx] at hF
Cleared hypotheses: hF, this, hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (hypothesis)
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
⊢ Cauchy (α := L) (map (fun (x : L) ↦ x⁻¹) F)
have hx' : x ≠ 0
Tactic: have hx' : x ≠ 0 := by
      rintro rfl
      rw [inf_eq_right.mpr hx] at hF
      exact cau_F.1.ne hF
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
⊢ CompletableTopField α
have refine : ∀ (F : Filter α) (F_cau : Cauchy F) (inf_F : 𝓝 0 ⊓ F = ⊥), Cauchy (α := α) (map (fun (x : α) ↦ x⁻¹) F)
Tactic: refine CompletableTopField.mk (fun F F_cau inf_F => ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy F
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy (α := α) (map (fun (x : α) ↦ x⁻¹) F)
have rw : ∀ (F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)) (inf_F : 𝓝 0 ⊓ F = ⊥),
  Cauchy.{u_4} (α := β) (map (α := α) (⇑f : (a : α) → β) (map (fun (x : α) ↦ x⁻¹) F))
Tactic: rw [← IsUniformInducing.cauchy_map_iff hf] at F_cau ⊢
Cleared hypotheses: F_cau, inf_F
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
have h : ∀ (x : α),
  Eq.{u_4 + 1} (α := β) (Function.comp (β := α) (⇑f : (a : α) → β) (fun (x : α) ↦ x⁻¹) x)
    (((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (hypothesis)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
⊢ Cauchy.{u_4} (α := β) (map (α := α) (⇑f : (a : α) → β) (map (fun (x : α) ↦ x⁻¹) F))
have h_comm : Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹) ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
Tactic: have h_comm : (f ∘ fun x => x⁻¹) = (fun x => x⁻¹) ∘ f := by
    ext; simp only [Function.comp_apply, map_inv₀]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
⊢ Cauchy.{u_4} (α := β) (map (α := α) (⇑f : (a : α) → β) (map (fun (x : α) ↦ x⁻¹) F))
have rw : Cauchy.{u_4} (α := β) (map (fun (x : β) ↦ x⁻¹) (map (⇑f : (a : α) → β) F))
Tactic: rw [Filter.map_comm h_comm]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
⊢ Cauchy.{u_4} (α := β) (map (fun (x : β) ↦ x⁻¹) (map (⇑f : (a : α) → β) F))
have apply : Eq.{u_4 + 1} (α := Filter β) (𝓝 0 ⊓ map (⇑f : (a : α) → β) F) ⊥
Tactic: apply CompletableTopField.nice _ F_cau
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
⊢ Eq.{u_4 + 1} (α := Filter β) (𝓝 0 ⊓ map (⇑f : (a : α) → β) F) ⊥
have rw : Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (Filter.comap.{u_3, u_4} (β := β) (⇑f : (a : α) → β) (𝓝 0) ⊓ F)) ⊥
Tactic: rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
rw :
  Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (Filter.comap.{u_3, u_4} (β := β) (⇑f : (a : α) → β) (𝓝 0) ⊓ F))
    ⊥
⊢ Eq.{u_4 + 1} (α := Filter β) (𝓝 0 ⊓ map (⇑f : (a : α) → β) F) ⊥
have rw₁ : Eq.{u_4 + 1} (α := Filter β)
  (map (⇑f : (a : α) → β)
    (Filter.comap.{u_3, u_4} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (𝓝 ((f : (a : α) → β) 0) : Filter β) ⊓ F))
  ⊥
Tactic: rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
rw :
  Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (Filter.comap.{u_3, u_4} (β := β) (⇑f : (a : α) → β) (𝓝 0) ⊓ F))
    ⊥
rw₁ :
  Eq.{u_4 + 1} (α := Filter β)
    (map (⇑f : (a : α) → β)
      (Filter.comap.{u_3, u_4} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (𝓝 ((f : (a : α) → β) 0) : Filter β) ⊓ F))
    ⊥
⊢ Eq.{u_4 + 1} (α := Filter β) (𝓝 0 ⊓ map (⇑f : (a : α) → β) F) ⊥
have rw₂ : Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (𝓝 0 ⊓ F)) ⊥
Tactic: rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
rw :
  Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (Filter.comap.{u_3, u_4} (β := β) (⇑f : (a : α) → β) (𝓝 0) ⊓ F))
    ⊥
rw₁ :
  Eq.{u_4 + 1} (α := Filter β)
    (map (⇑f : (a : α) → β)
      (Filter.comap.{u_3, u_4} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (𝓝 ((f : (a : α) → β) 0) : Filter β) ⊓ F))
    ⊥
rw₂ : Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (𝓝 0 ⊓ F)) ⊥
⊢ Eq.{u_4 + 1} (α := Filter β) (𝓝 0 ⊓ map (⇑f : (a : α) → β) F) ⊥
have rw₃ : Eq.{u_4 + 1} (α := Filter β) (map.{u_3, u_4} (α := α) (⇑f : (a : α) → β) ⊥) ⊥
Tactic: rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformField (goal)
Goal:
α : Type u_3
β : Type u_4
inst : Field β
b : UniformSpace β
inst_1 : CompletableTopField β
inst_2 : Field α
inst_3 : UniformSpace α
inst_4 : T0Space α
f : α →+* β
hf : IsUniformInducing.{u_3, u_4} (α := α) (β := β) (⇑f : (a : α) → β)
F : Filter α
F_cau : Cauchy.{u_4} (α := β) (map (⇑f : (a : α) → β) F)
inf_F : 𝓝 0 ⊓ F = ⊥
h_comm :
  Eq (α := α → β) (Function.comp (β := α) (⇑f : (a : α) → β) fun (x : α) ↦ x⁻¹)
    ((fun (x : β) ↦ x⁻¹) ∘ (⇑f : (a : α) → β))
rw :
  Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (Filter.comap.{u_3, u_4} (β := β) (⇑f : (a : α) → β) (𝓝 0) ⊓ F))
    ⊥
rw₁ :
  Eq.{u_4 + 1} (α := Filter β)
    (map (⇑f : (a : α) → β)
      (Filter.comap.{u_3, u_4} (β := β) ((⇑f : (a : α) → β) : (a : α) → β) (𝓝 ((f : (a : α) → β) 0) : Filter β) ⊓ F))
    ⊥
rw₂ : Eq.{u_4 + 1} (α := Filter β) (map (⇑f : (a : α) → β) (𝓝 0 ⊓ F)) ⊥
rw₃ : Eq.{u_4 + 1} (α := Filter β) (map.{u_3, u_4} (α := α) (⇑f : (a : α) → β) ⊥) ⊥
⊢ Eq.{u_4 + 1} (α := Filter β) (𝓝 0 ⊓ map (⇑f : (a : α) → β) F) ⊥
have rw₄ : Eq.{u_4 + 1} (α := Filter β) ⊥ ⊥
Tactic: rw [← Filter.push_pull', ← map_zero f, ← hf.isInducing.nhds_eq_comap, inf_F, Filter.map_bot]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (hypothesis)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this : UniformSpace G := B.uniformSpace
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have this₁ : IsUniformAddGroup G
Tactic: haveI := B.isUniformAddGroup
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mpr : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : F ×ˢ F ≤ uniformity G
⊢ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mp : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Tactic: refine ⟨h', ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
h' : F.NeBot
h : ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F
have mpr : F ×ˢ F ≤ uniformity G
Tactic: refine ⟨h', ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
Tactic: constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]
-- Lean 4 proof step from Mathlib.Topology.Algebra.UniformFilterBasis (goal)
Goal:
G : Type u_1
inst : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this_1 : UniformSpace G := B.uniformSpace
this_2 : IsUniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
mp : Cauchy F → F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
⊢ Cauchy F ↔ F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U
have mpr : (F.NeBot ∧ ∀ U ∈ B, ∃ M ∈ F, ∀ x ∈ M, ∀ y ∈ M, y - x ∈ U) → Cauchy F
Tactic: constructor <;> rintro ⟨h', h⟩ <;> refine ⟨h', ?_⟩ <;> [rwa [← this]; rwa [this]]