awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
open : 𝓝 s ≤ Filter.comap (Prod.mk s) (𝓤 (Set α))
open₁ :
  ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i' ∈ 𝓝 s
open₂ : ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → Prod.mk s ⁻¹' hausdorffEntourage i' ∈ 𝓝 s
open₃ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      Prod.mk s ⁻¹' {x : Set α × Set α | x.1 ⊆ i'.preimage x.2 ∧ x.2 ⊆ i'.image x.1} ∈ 𝓝 s
open₄ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a : Set α | s ⊆ i'.preimage a ∧ a ⊆ i'.image s} ∈ 𝓝 s
open₅ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      {a : Set α | s ⊆ i'.preimage a} ∩ {a : Set α | a ⊆ i'.image s} ∈ 𝓝 s
open₆ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
open₇ open₈ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
⊢ 𝓝 s ≤ 𝓝 s
have open₉ : ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl),
  {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
Tactic: open UniformSpace TopologicalSpace.vietoris in
  simp_rw [nhds_eq_comap_uniformity,
    uniformity_hasBasis_open.uniformity_hausdorff |>.comap _ |>.ge_iff, Function.comp_id,
    hausdorffEntourage, Set.preimage_setOf_eq, Set.setOf_and]
  intro U ⟨hU₁, hU₂⟩
  have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
  let := TopologicalSpace.vietoris α
  refine Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
    SetRel.self_subset_image _
  obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁
  obtain ⟨t, ht₁, ht₂⟩ := hs.exists_prodMk_finset_mem_hausdorffEntourage hV₁
  dsimp only at ht₁ ht₂
  filter_upwards [(Filter.eventually_all_finset t).mpr fun x hx =>
    isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (ht₁ hx)]
    with u (hu : ↑t ⊆ V.preimage ↑u)
  grw [ht₂, ← SetRel.preimage_eq_image, hu, ← hVU, SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
open : 𝓝 s ≤ Filter.comap (Prod.mk s) (𝓤 (Set α))
open₁ :
  ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i' ∈ 𝓝 s
open₂ : ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → Prod.mk s ⁻¹' hausdorffEntourage i' ∈ 𝓝 s
open₃ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      Prod.mk s ⁻¹' {x : Set α × Set α | x.1 ⊆ i'.preimage x.2 ∧ x.2 ⊆ i'.image x.1} ∈ 𝓝 s
open₄ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a : Set α | s ⊆ i'.preimage a ∧ a ⊆ i'.image s} ∈ 𝓝 s
open₅ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      {a : Set α | s ⊆ i'.preimage a} ∩ {a : Set α | a ⊆ i'.image s} ∈ 𝓝 s
open₆ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
open₇ open₈ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
open₉ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl),
    {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
⊢ 𝓝 s ≤ 𝓝 s
have open₁₀ : ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl) (V : SetRel α α)
  (hV₁ : V ∈ 𝓤 α) (hV₂ : IsOpen[instTopologicalSpaceProd] V),
  V.IsSymm → ∀ (hVU : V.comp V ⊆ U), {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
Tactic: open UniformSpace TopologicalSpace.vietoris in
  simp_rw [nhds_eq_comap_uniformity,
    uniformity_hasBasis_open.uniformity_hausdorff |>.comap _ |>.ge_iff, Function.comp_id,
    hausdorffEntourage, Set.preimage_setOf_eq, Set.setOf_and]
  intro U ⟨hU₁, hU₂⟩
  have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
  let := TopologicalSpace.vietoris α
  refine Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
    SetRel.self_subset_image _
  obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁
  obtain ⟨t, ht₁, ht₂⟩ := hs.exists_prodMk_finset_mem_hausdorffEntourage hV₁
  dsimp only at ht₁ ht₂
  filter_upwards [(Filter.eventually_all_finset t).mpr fun x hx =>
    isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (ht₁ hx)]
    with u (hu : ↑t ⊆ V.preimage ↑u)
  grw [ht₂, ← SetRel.preimage_eq_image, hu, ← hVU, SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : TotallyBounded s
open : 𝓝 s ≤ Filter.comap (Prod.mk s) (𝓤 (Set α))
open₁ :
  ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → Prod.mk s ⁻¹' (hausdorffEntourage ∘ id) i' ∈ 𝓝 s
open₂ : ∀ (i' : SetRel α α), i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → Prod.mk s ⁻¹' hausdorffEntourage i' ∈ 𝓝 s
open₃ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      Prod.mk s ⁻¹' {x : Set α × Set α | x.1 ⊆ i'.preimage x.2 ∧ x.2 ⊆ i'.image x.1} ∈ 𝓝 s
open₄ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' → {a : Set α | s ⊆ i'.preimage a ∧ a ⊆ i'.image s} ∈ 𝓝 s
open₅ :
  ∀ (i' : SetRel α α),
    i' ∈ 𝓤 α ∧ IsOpen[instTopologicalSpaceProd] i' →
      {a : Set α | s ⊆ i'.preimage a} ∩ {a : Set α | a ⊆ i'.image s} ∈ 𝓝 s
open₆ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
open₇ open₈ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl),
    {a : Set α | s ⊆ U.preimage a} ∩ {a : Set α | a ⊆ U.image s} ∈ 𝓝 s
open₉ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl),
    {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
open₁₀ :
  ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl) (V : SetRel α α)
    (hV₁ : V ∈ 𝓤 α) (hV₂ : IsOpen[instTopologicalSpaceProd] V),
    V.IsSymm → ∀ (hVU : V.comp V ⊆ U), {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
⊢ 𝓝 s ≤ 𝓝 s
have open₁₁ : ∀ (U : SetRel α α) (hU₁ : U ∈ 𝓤 α) (hU₂ : IsOpen[instTopologicalSpaceProd] U) (this : U.IsRefl) (V : SetRel α α)
  (hV₁ : V ∈ 𝓤 α) (hV₂ : IsOpen[instTopologicalSpaceProd] V),
  V.IsSymm →
    ∀ (hVU : V.comp V ⊆ U) (t : Finset α) (ht₁ : ((↑t : Set α), s).1 ⊆ V.preimage ((↑t : Set α), s).2)
      (ht₂ : ((↑t : Set α), s).2 ⊆ V.image ((↑t : Set α), s).1), {a : Set α | s ⊆ U.preimage a} ∈ 𝓝 s
Tactic: open UniformSpace TopologicalSpace.vietoris in
  simp_rw [nhds_eq_comap_uniformity,
    uniformity_hasBasis_open.uniformity_hausdorff |>.comap _ |>.ge_iff, Function.comp_id,
    hausdorffEntourage, Set.preimage_setOf_eq, Set.setOf_and]
  intro U ⟨hU₁, hU₂⟩
  have : U.IsRefl := ⟨fun _ => refl_mem_uniformity hU₁⟩
  let := TopologicalSpace.vietoris α
  refine Filter.inter_mem ?_ <| hU₂.relImage.powerset_vietoris.mem_nhds <|
    SetRel.self_subset_image _
  obtain ⟨V : SetRel α α, hV₁, hV₂, _, hVU⟩ := comp_open_symm_mem_uniformity_sets hU₁
  obtain ⟨t, ht₁, ht₂⟩ := hs.exists_prodMk_finset_mem_hausdorffEntourage hV₁
  dsimp only at ht₁ ht₂
  filter_upwards [(Filter.eventually_all_finset t).mpr fun x hx =>
    isOpen_inter_nonempty_of_isOpen (isOpen_ball x hV₂) |>.eventually_mem (ht₁ hx)]
    with u (hu : ↑t ⊆ V.preimage ↑u)
  grw [ht₂, ← SetRel.preimage_eq_image, hu, ← hVU, SetRel.preimage_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
⊢ 𝓝 s = 𝓝 s
have refine : 𝓝 s ≤ 𝓝 s
Tactic: refine le_antisymm ?_ hs.totallyBounded.nhds_vietoris_le_nhds_hausdorff
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
⊢ 𝓝 s ≤ 𝓝 s
have simp_rw : ∀ (i : Set (Set α))
  (j :
    Membership.mem (γ := Set (Set (Set α)))
      {s_1 : Set (Set α) |
        s ∈ s_1 ∧
          Membership.mem (γ := Set (Set (Set α)))
            (Set.powerset '' {U : Set α | IsOpen[inst.toTopologicalSpace] U} ∪
              (fun (V : Set α) ↦ {s : Set α | (s ∩ V).Nonempty}) '' {U : Set α | IsOpen[inst.toTopologicalSpace] U})
            s_1}
      i),
  i ∈ 𝓝 s
Tactic: simp_rw [TopologicalSpace.nhds_generateFrom, le_iInf₂_iff, Filter.le_principal_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : s ∈ 𝒫 U
⊢ 𝒫 U ∈ 𝓝 s
have inl : ∀ (V : SetRel α α) (hV₁ : V ∈ 𝓤 α) (hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U), 𝒫 U ∈ 𝓝 s
Tactic: obtain ⟨V : SetRel α α, hV₁, hV₂⟩ :=
      hs.nhdsSet_basis_uniformity (𝓤 α).basis_sets |>.mem_iff.mp (hU.mem_nhdsSet.mpr hs')
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
t : Set α
⊢ t ∈ UniformSpace.ball s (hausdorffEntourage V) → t ∈ 𝒫 U
have h : (s, t).1 ⊆ V.preimage (s, t).2 → ∀ (ht : (s, t).2 ⊆ V.image (s, t).1), t ∈ 𝒫 U
Tactic: ⟨_, ht⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
s : Set α
hs : IsCompact s
U : Set α
hU : Membership.mem (γ := Set (Set α)) {U : Set α | IsOpen[inst.toTopologicalSpace] U} U
hs' : s ∈ 𝒫 U
V : SetRel α α
hV₁ : V ∈ 𝓤 α
hV₂ : ⋃ x ∈ s, UniformSpace.ball x (id V) ⊆ U
⊢ 𝒫 U ∈ 𝓝 s
have h : ∀ (t : Set α), (s, t).1 ⊆ V.preimage (s, t).2 → ∀ (ht : (s, t).2 ⊆ V.image (s, t).1), t ∈ 𝒫 U
Tactic: filter_upwards [UniformSpace.ball_mem_nhds _ (Filter.mem_lift' hV₁)]
      with t ⟨_, ht⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompactSpace α
⊢ IsCompact.{u_1} (X := Set α) Set.univ
have rw : ∀ (f : Ultrafilter (Set α)),
  (↑f : Filter (Set α)) ≤ 𝓟 Set.univ →
    ∃ (x : Set α), Membership.mem (γ := Set (Set α)) Set.univ x ∧ (↑f : Filter (Set α)) ≤ 𝓝 x
Tactic: rw [isCompact_iff_ultrafilter_le_nhds]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompactSpace α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
⊢ ∃ (x : Set α), Membership.mem (γ := Set (Set α)) Set.univ x ∧ (↑f : Filter (Set α)) ≤ 𝓝 x
have refine : (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
Tactic: refine ⟨closure f.lim, Set.mem_univ _, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompactSpace α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
⊢ (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
have grw : (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
Tactic: grw [isClosed_closure.isCompact.nhds_hausdorff_eq_nhds_vietoris,
      ← TopologicalSpace.vietoris.specializes_closure.nhds_le_nhds, f.le_nhds_lim]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompactSpace α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
grw : (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
⊢ (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
have grw₁ : (↑f : Filter (Set α)) ≤ 𝓝 f.lim
Tactic: grw [isClosed_closure.isCompact.nhds_hausdorff_eq_nhds_vietoris,
      ← TopologicalSpace.vietoris.specializes_closure.nhds_le_nhds, f.le_nhds_lim]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompactSpace α
f : Ultrafilter (Set α)
this : TopologicalSpace (Set α) := TopologicalSpace.vietoris α
grw : (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
grw₁ : (↑f : Filter (Set α)) ≤ 𝓝 f.lim
⊢ (↑f : Filter (Set α)) ≤ 𝓝 (closure[inst.toTopologicalSpace] f.lim)
have grw₂ : 𝓝 f.lim ≤ 𝓝 f.lim
Tactic: grw [isClosed_closure.isCompact.nhds_hausdorff_eq_nhds_vietoris,
      ← TopologicalSpace.vietoris.specializes_closure.nhds_le_nhds, f.le_nhds_lim]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ IsClopen (X := Closeds α) {⊥}
have h : Eq (α := Set (Closeds α)) {⊥} (SetLike.coe ⁻¹' {∅})
Tactic: convert! UniformSpace.hausdorff.isClopen_singleton_empty.preimage uniformContinuous_coe.continuous
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ Eq (α := Set (Closeds α)) {⊥} (SetLike.coe ⁻¹' {∅})
have h : ∀ (x : Closeds α),
  Membership.mem (γ := Set (Closeds α)) {⊥} x ↔ Membership.mem (γ := Set (Closeds α)) (SetLike.coe ⁻¹' {∅}) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T0Space α
⊢ IsClosed.{u_1} (X := Closeds α) (Set.range fun (x : α) ↦ {x})
have rw : IsClosed (X := Closeds α)
  (SetLike.coe ⁻¹' Set.range (ι := α) (Function.comp (β := Closeds α) SetLike.coe fun (x : α) ↦ {x}))
Tactic: rw [← SetLike.coe_injective.preimage_image (s := Set.range ({·})), ← Set.range_comp]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
⊢ T0Space.{u_1} (Closeds α)
have suffices : ∀ (F₁ F₂ : Closeds α), Inseparable F₁ F₂ → F₁ ≤ F₂
Tactic: suffices ∀ F₁ F₂ : Closeds α, Inseparable F₁ F₂ → F₁ ≤ F₂ from
    ⟨fun F₁ F₂ h => le_antisymm (this F₁ F₂ h) (this F₂ F₁ h.symm)⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
⊢ ∀ (F₁ F₂ : Closeds α), Inseparable F₁ F₂ → F₁ ≤ F₂
have refine : ∀ (F₁ F₂ : Closeds α) (h : Inseparable F₁ F₂) (x : α) (hx₁ : x ∈ F₁), ∃ᶠ (y : α) in 𝓝 x, y ∈ (↑F₂ : Set α)
Tactic: refine fun F₁ F₂ h x hx₁ => isClosed_iff_frequently.mp F₂.isClosed _ ?_
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
⊢ ∃ᶠ (y : α) in 𝓝 x, y ∈ (↑F₂ : Set α)
have rw : ∀ {U : Set (α × α)}, U ∈ 𝓤 α → ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)
Tactic: rw [nhds_eq_comap_uniformity, Filter.frequently_comap, Filter.frequently_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
F₁ F₂ : Closeds α
h : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)
have h₁ : (↑F₁ : Set α) ⊆ U.preimage (↑F₂ : Set α)
Tactic: obtain ⟨h : (F₁ : Set α) ⊆ U.preimage F₂, -⟩ :=
    mem_of_mem_nhds <| h.nhds_le_uniformity <| Filter.preimage_mem_comap <| Filter.mem_lift' hU
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
F₁ F₂ : Closeds α
h_1 : Inseparable F₁ F₂
x : α
hx₁ : x ∈ F₁
U : SetRel α α
hU : U ∈ 𝓤 α
h : (↑F₁ : Set α) ⊆ U.preimage (↑F₂ : Set α)
⊢ ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)
have obtain : ∀ (y : α) (hy : y ∈ (↑F₂ : Set α)) (hxy : (x, y) ∈ U), ∃ x_1 ∈ U, ∃ (a : α), (x, a) = x_1 ∧ a ∈ (↑F₂ : Set α)
Tactic: obtain ⟨y, hy, hxy⟩ := h hx₁
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ CompactSpace.{u_1} (Closeds α) ↔ CompactSpace α
have refine : CompactSpace.{u_1} (Closeds α) →
  ∀ {ι : Type u_1} (F : ι → Set α) (hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i))
    (hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅), ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅
Tactic: refine ⟨fun _ => compactSpace_of_finite_subfamily_closed fun {ι} F hF₁ hF₂ => ?_,
    fun _ => inferInstance⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
⊢ ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅
have this : ∀
  (hst :
    Eq (α := Set (Closeds α))
      ({⊥}ᶜ ∩ ⋂ (i : ι), (fun (i : ι) ↦ ({C : Closeds α | (↑C : Set α) ⊆ F i} : Set (Closeds α))) i) ∅),
  ∃ (u : Finset ι),
    Eq (α := Set (Closeds α))
      ({⊥}ᶜ ∩ ⋂ i ∈ u, (fun (i : ι) ↦ ({C : Closeds α | (↑C : Set α) ⊆ F i} : Set (Closeds α))) i) ∅
Tactic: have := isClopen_singleton_bot.compl.isClosed.isCompact.elim_finite_subfamily_closed
    (fun i => {C : Closeds α | ↑C ⊆ F i})
    (fun i => isClosed_subsets_of_isClosed (hF₁ i))
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
this :
  ∀
    (hst :
      Eq (α := Set (Closeds α))
        ({⊥}ᶜ ∩ ⋂ (i : ι), (fun (i : ι) ↦ ({C : Closeds α | (↑C : Set α) ⊆ F i} : Set (Closeds α))) i) ∅),
    ∃ (u : Finset ι),
      Eq (α := Set (Closeds α))
        ({⊥}ᶜ ∩ ⋂ i ∈ u, (fun (i : ι) ↦ ({C : Closeds α | (↑C : Set α) ⊆ F i} : Set (Closeds α))) i) ∅
⊢ ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅
have this₁ : ∀ (hst : Subset (α := Set (Closeds α)) {⊥} {⊥}),
  ∃ (u : Finset ι), Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ u, F i} {⊥}
Tactic: simp_rw [← Set.disjoint_iff_inter_eq_empty, Set.disjoint_compl_left_iff_subset,
    ← Set.setOf_forall, ← Set.subset_iInter_iff, hF₂, Set.subset_empty_iff, coe_eq_empty,
    Set.setOf_eq_eq_singleton] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
this :
  ∀ (hst : Subset (α := Set (Closeds α)) {⊥} {⊥}),
    ∃ (u : Finset ι), Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ u, F i} {⊥}
⊢ ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅
have obtain : ∀ (s : Finset ι) (hs : Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ s, F i} {⊥}),
  ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅
Tactic: obtain ⟨s, hs⟩ := this .rfl
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompactSpace.{u_1} (Closeds α)
ι : Type u_1
F : ι → Set α
hF₁ : ∀ (i : ι), IsClosed[inst.toTopologicalSpace] (F i)
hF₂ : Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), F i) ∅
this :
  ∀ (hst : Subset (α := Set (Closeds α)) {⊥} {⊥}),
    ∃ (u : Finset ι), Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ u, F i} {⊥}
s : Finset ι
hs : Subset (α := Set (Closeds α)) {x : Closeds α | (↑x : Set α) ⊆ ⋂ i ∈ s, F i} {⊥}
⊢ ∃ (u : Finset ι), Eq.{u_1 + 1} (α := Set α) (⋂ i ∈ u, F i) ∅
have hs₁ : Membership.mem (γ := Set (Closeds α)) {⊥} { carrier := ⋂ i ∈ s, F i, isClosed' := sorry }
Tactic: specialize @hs ⟨⋂ i ∈ s, F i, isClosed_biInter fun i _ => hF₁ i⟩ .rfl
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
⊢ NoncompactSpace.{u_1} (Closeds α) ↔ NoncompactSpace α
have simp_rw : ¬CompactSpace.{u_1} (Closeds α) ↔ ¬CompactSpace α
Tactic: simp_rw [← not_compactSpace_iff, compactSpace_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
K : Compacts α
⊢ 𝓝 K = 𝓝 K
have simp_rw : Eq (α := Filter (Compacts α)) (Filter.comap SetLike.coe (𝓝 (↑K : Set α))) (Filter.comap SetLike.coe (𝓝 (↑K : Set α)))
Tactic: simp_rw [nhds_induced, K.isCompact.nhds_hausdorff_eq_nhds_vietoris]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
inst_1 : T2Space α
inst_2 : CompleteSpace α
⊢ IsClosed.{u_1} (X := Closeds α) (Set.range toCloseds)
have h : Eq.{u_1 + 1} (α := Set (Closeds α)) (Set.range toCloseds) {s : Closeds α | TotallyBounded (↑s : Set α)}
Tactic: convert! Closeds.isClosed_setOf_totallyBounded
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
⊢ CompleteSpace.{u_1} (Compacts α)
have refine : ∀ {f : Filter (Compacts α)}, Cauchy f → f.NeBot → ∀ (hf : f ×ˢ f ≤ 𝓤 (Compacts α)), ∃ (x : Compacts α), f ≤ 𝓝 x
Tactic: refine ⟨fun {f} ⟨_, hf⟩ => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf : f ×ˢ f ≤ 𝓤 (Compacts α)
⊢ ∃ (x : Compacts α), f ≤ 𝓝 x
have hf₁ : ∀ i' ∈ 𝓤 α, Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i') ∈ f.curry f
Tactic: grw [← Filter.curry_le_prod, (𝓤 α).basis_sets.uniformity_compacts.ge_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (hypothesis)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf : ∀ i' ∈ 𝓤 α, Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i') ∈ f.curry f
⊢ ∃ (x : Compacts α), f ≤ 𝓝 x
have hf₁ : ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
  ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
Tactic: change ∀ {U} (hU : U ∈ 𝓤 α), ∀ᶠ K in f, ∀ᶠ K' in f, (↑K, ↑K') ∈ hausdorffEntourage U at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
f : Filter (Compacts α)
h : Cauchy f
left : f.NeBot
hf :
  ∀ {U : Set (α × α)} (hU : U ∈ 𝓤 α),
    ∀ᶠ (K : Compacts α) (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
l : Filter α := f.lift' fun (s : Set (Compacts α)) ↦ ⋃ K ∈ s, (↑K : Set α)
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
have obtain : ∀ (V : SetRel α α) (hV : V ∈ 𝓤 α) (hVU : V.comp V ⊆ U), ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
Tactic: obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU