awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
have obtain : ∀ (K : Compacts α)
  (hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)),
  ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
Tactic: obtain ⟨K, hK⟩ := hf (symm_le_uniformity hV) |>.exists
-- 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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
have obtain : ∀ (t : Set α) (ht₁ : t.Finite) (ht₂ : (↑K : Set α) ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ V}),
  ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
Tactic: obtain ⟨t, ht₁, ht₂⟩ := K.isCompact.totallyBounded V hV
-- 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 :
  ∀ {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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ ⋃ y ∈ t, {x : α | (x, y) ∈ V}
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
have ht₃ : (↑K : Set α) ⊆ V.preimage t
Tactic: rw [← SetRel.preimage_eq_biUnion] at ht₂
Cleared hypotheses: 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 : 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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
⊢ ∃ (t : Set α), t.Finite ∧ U.preimage t ∈ l
have refine : ⋃ (K_1 : Compacts α),
    ⋃ (_ :
      Membership.mem (γ := Set (Compacts α))
        {x : Compacts α |
          (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}
        K_1),
      (↑K_1 : Set α) ⊆
  U.preimage t
Tactic: refine ⟨t, ht₁, Filter.mem_of_superset (Filter.mem_lift' hK) ?_⟩
-- 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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
⊢ ⋃ (K_1 : Compacts α),
      ⋃ (_ :
        Membership.mem (γ := Set (Compacts α))
          {x : Compacts α |
            (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}
          K_1),
        (↑K_1 : Set α) ⊆
    U.preimage t
have rw : ∀ (i : Compacts α)
  (j :
    Membership.mem (γ := Set (Compacts α))
      {x : Compacts α |
        (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}
      i),
  (↑i : Set α) ⊆ U.preimage t
Tactic: rw [Set.iUnion₂_subset_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 γ
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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
K' : Compacts α
⊢ ∀
    (j :
      Membership.mem (γ := Set (Compacts α))
        {x : Compacts α |
          (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)) x}
        K'),
    (↑K' : Set α) ⊆ U.preimage t
have this : ((↑K : Set α), (↑K' : Set α)).1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) ((↑K : Set α), (↑K' : Set α)).2 →
  ∀ (hK' : (↑K' : Set α) ⊆ V.preimage (↑K : Set α)), (↑K' : Set α) ⊆ U.preimage t
Tactic: ⟨_, (hK' : ↑K' ⊆ V.preimage K)⟩
-- 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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
K' : Compacts α
left_1 : ((↑K : Set α), (↑K' : Set α)).1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) ((↑K : Set α), (↑K' : Set α)).2
hK' : (↑K' : Set α) ⊆ V.preimage (↑K : Set α)
⊢ (↑K' : Set α) ⊆ U.preimage t
have grw : (↑K' : Set α) ⊆ (V.comp V).preimage t
Tactic: grw [← hVU, SetRel.preimage_comp, ← ht₂, hK']
-- 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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
K' : Compacts α
left_1 : ((↑K : Set α), (↑K' : Set α)).1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) ((↑K : Set α), (↑K' : Set α)).2
hK' : (↑K' : Set α) ⊆ V.preimage (↑K : Set α)
grw : (↑K' : Set α) ⊆ (V.comp V).preimage t
⊢ (↑K' : Set α) ⊆ U.preimage t
have grw₁ : (↑K' : Set α) ⊆ V.preimage (V.preimage t)
Tactic: grw [← hVU, SetRel.preimage_comp, ← ht₂, hK']
-- 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 ∈ 𝓤 α
V : SetRel α α
hV : V ∈ 𝓤 α
hVU : V.comp V ⊆ U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage (Prod.swap ⁻¹' V)
t : Set α
ht₁ : t.Finite
ht₂ : (↑K : Set α) ⊆ V.preimage t
K' : Compacts α
left_1 : ((↑K : Set α), (↑K' : Set α)).1 ⊆ SetRel.preimage (Prod.swap ⁻¹' V) ((↑K : Set α), (↑K' : Set α)).2
hK' : (↑K' : Set α) ⊆ V.preimage (↑K : Set α)
grw : (↑K' : Set α) ⊆ (V.comp V).preimage t
grw₁ : (↑K' : Set α) ⊆ V.preimage (V.preimage t)
grw₂ : (↑K' : Set α) ⊆ V.preimage (↑K : Set α)
⊢ (↑K' : Set α) ⊆ U.preimage t
have grw₃ : V.preimage (↑K : Set α) ⊆ V.preimage (↑K : Set α)
Tactic: grw [← hVU, SetRel.preimage_comp, ← ht₂, hK']
-- 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 :
  ∀ {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 α)
⊢ ∃ (x : Compacts α), f ≤ 𝓝 x
have hl : l.TotallyBounded
Tactic: have hl : l.TotallyBounded := by
    intro U hU
    obtain ⟨V : SetRel α α, hV, hVU⟩ := comp_mem_uniformity_sets hU
    obtain ⟨K, hK⟩ := hf (symm_le_uniformity hV) |>.exists
    obtain ⟨t, ht₁, ht₂⟩ := K.isCompact.totallyBounded V hV
    rw [← SetRel.preimage_eq_biUnion] at ht₂
    refine ⟨t, ht₁, Filter.mem_of_superset (Filter.mem_lift' hK) ?_⟩
    rw [Set.iUnion₂_subset_iff]
    intro K' ⟨_, (hK' : ↑K' ⊆ V.preimage K)⟩
    grw [← hVU, SetRel.preimage_comp, ← ht₂, hK']
-- 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
⊢ ∃ (x : Compacts α), f ≤ 𝓝 x
have exists : f ≤ 𝓝 L
Tactic: exists L
-- 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
⊢ f ≤ 𝓝 L
have simp_rw : f ≤ Filter.comap (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L)) (𝓤 (Compacts α))
Tactic: simp_rw [nhds_eq_comap_uniformity']
-- 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
⊢ f ≤ Filter.comap (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L)) (𝓤 (Compacts α))
have rw : ∀ (i' : SetRel α α),
  i' ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] i' →
    Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
        (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id i')) ∈
      f
Tactic: rw [uniformity_hasBasis_closed.uniformity_compacts.comap _ |>.ge_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 γ
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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
⊢ U ∈ 𝓤 α ∧ IsClosed[instTopologicalSpaceProd] U →
    Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
        (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)) ∈
      f
have this : ∀ (hU₁ : U ∈ 𝓤 α) (hU₂ : IsClosed[instTopologicalSpaceProd] U),
  Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
      (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)) ∈
    f
Tactic: ⟨hU₁, 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 γ
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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
⊢ Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
      (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)) ∈
    f
have h : ∀ (K : Compacts α) (hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U),
  Membership.mem (γ := Set (Compacts α))
    (Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
      (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)))
    K
Tactic: filter_upwards [hf hU₁] with K hK
-- 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
⊢ Membership.mem (γ := Set (Compacts α))
    (Set.preimage (β := Compacts α × Compacts α) (fun (y : Compacts α) ↦ (y, L))
      (Prod.map SetLike.coe SetLike.coe ⁻¹' hausdorffEntourage (id U)))
    K
have h : (↑K : Set α) ⊆ U.preimage (↑L : Set α) ∧ (↑L : Set α) ⊆ U.image (↑K : Set α)
Tactic: simp_rw [Set.mem_preimage, Prod.map, id, mem_hausdorffEntourage]
-- 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
⊢ (↑K : Set α) ⊆ U.preimage (↑L : Set α) ∧ (↑L : Set α) ⊆ U.image (↑K : Set α)
have h : (↑K : Set α) ⊆ U.preimage (↑L : Set α)
Tactic: constructor
-- 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_1 : 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
h : (↑K : Set α) ⊆ U.preimage (↑L : Set α)
⊢ (↑K : Set α) ⊆ U.preimage (↑L : Set α) ∧ (↑L : Set α) ⊆ U.image (↑K : Set α)
have h₁ : (↑L : Set α) ⊆ U.image (↑K : Set α)
Tactic: constructor
-- 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 :
  ∀ {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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
⊢ x ∈ U.preimage (↑L : Set α)
have le_def : let lx := l ⊓ 𝓟 (UniformSpace.ball x U);
lx = l ⊓ 𝓟 (UniformSpace.ball x U)
Tactic: set lx := l ⊓ 𝓟 (UniformSpace.ball x U) with le_def
-- 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 :
  ∀ {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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
⊢ x ∈ U.preimage (↑L : Set α)
have hlx : lx.TotallyBounded
Tactic: have hlx : lx.TotallyBounded := hl.mono inf_le_left
-- 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
⊢ lx.NeBot
have rw : ∀ s ∈ f, ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty
Tactic: rw [le_def, Filter.lift'_inf_principal_eq, Filter.lift'_neBot_iff fun _ _ h =>
        Set.inter_subset_inter_left _ <| Set.biUnion_subset_biUnion_left h]
-- 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
s : Set (Compacts α)
hs : s ∈ f
⊢ ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty
have obtain : ∀ (K' : Compacts α) (h₂ : K' ∈ s) (h₁ : ((↑K : Set α), (↑K' : Set α)).1 ⊆ U.preimage ((↑K : Set α), (↑K' : Set α)).2),
  ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty
Tactic: obtain ⟨K', ⟨h₁, -⟩, h₂⟩ := Filter.nonempty_of_mem <| Filter.inter_mem hK hs
-- 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 α)
hl : l.TotallyBounded
L : Compacts α := { carrier := {x : α | ClusterPt x l}, isCompact' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : x ∈ (↑K : Set α)
lx : Filter α := l ⊓ 𝓟 (UniformSpace.ball x U)
le_def : lx = l ⊓ 𝓟 (UniformSpace.ball x U)
hlx : lx.TotallyBounded
s : Set (Compacts α)
hs : s ∈ f
K' : Compacts α
h₂ : K' ∈ s
h₁ : ((↑K : Set α), (↑K' : Set α)).1 ⊆ U.preimage ((↑K : Set α), (↑K' : Set α)).2
⊢ ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty
have obtain : ∀ (y : α) (hy : y ∈ ((↑K : Set α), (↑K' : Set α)).2) (hxy : (x, y) ∈ U),
  ((⋃ K ∈ s, (↑K : Set α)) ∩ UniformSpace.ball x U).Nonempty
Tactic: obtain ⟨y, hy, hxy⟩ := h₁ hx