awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
hlx : lx.TotallyBounded
⊢ x ∈ U.preimage (↑L : Set α)
have this : lx.NeBot
Tactic: have : lx.NeBot := by
      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]
      intro s hs
      obtain ⟨K', ⟨h₁, -⟩, h₂⟩ := Filter.nonempty_of_mem <| Filter.inter_mem hK hs
      obtain ⟨y, hy, hxy⟩ := h₁ hx
      exact ⟨y, Set.mem_iUnion₂_of_mem h₂ hy, hxy⟩
-- 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
this : lx.NeBot
⊢ x ∈ U.preimage (↑L : Set α)
have h : ∀ (y : α) (hy : ClusterPt y lx), x ∈ U.preimage (↑L : Set α)
Tactic: obtain ⟨y, hy⟩ := hlx.exists_clusterPt
-- 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)
hlx : lx.TotallyBounded
this : lx.NeBot
y : α
hy : ClusterPt y lx
⊢ x ∈ U.preimage (↑L : Set α)
have hy₁ : ClusterPt y l
Tactic: have hy₁ : ClusterPt y l := .of_inf_left hy
-- 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)
hlx : lx.TotallyBounded
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
⊢ x ∈ U.preimage (↑L : Set α)
have hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U))
Tactic: have hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U)) := .of_inf_right hy
-- 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)
hlx : lx.TotallyBounded
this : lx.NeBot
y : α
hy : ClusterPt y lx
hy₁ : ClusterPt y l
hy₂ : ClusterPt y (𝓟 (UniformSpace.ball x U))
⊢ x ∈ U.preimage (↑L : Set α)
have hy₃ : y ∈ UniformSpace.ball x U
Tactic: rw [← mem_closure_iff_clusterPt, (UniformSpace.isClosed_ball x hU₂).closure_eq] at hy₂
Cleared hypotheses: hy₂
-- 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 : α
⊢ x ∈ (↑L : Set α) → x ∈ U.image (↑K : Set α)
have h : ∀ (hx : ClusterPt x l), x ∈ U.image (↑K : Set α)
Tactic: (hx : ClusterPt x 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' := ⋯ }
U : SetRel α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : ClusterPt x l
⊢ x ∈ U.image (↑K : Set α)
have h : ClusterPt x (𝓟 (U.image (↑K : Set α)))
Tactic: rw [← (hU₂.relImage_of_isCompact K.isCompact).closure_eq, mem_closure_iff_clusterPt]
-- 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 : ClusterPt x l
⊢ ClusterPt x (𝓟 (U.image (↑K : Set α)))
have h : l ≤ 𝓟 (U.image (↑K : Set α))
Tactic: refine hx.mono ?_
-- 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 : ClusterPt x l
⊢ l ≤ 𝓟 (U.image (↑K : Set α))
have h : U.image (↑K : Set α) ∈ l
Tactic: rw [Filter.le_principal_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 α α
hU₁ : U ∈ 𝓤 α
hU₂ : IsClosed[instTopologicalSpaceProd] U
K : Compacts α
hK : ∀ᶠ (K' : Compacts α) in f, ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U
x : α
hx : ClusterPt x l
⊢ U.image (↑K : Set α) ∈ l
have h : ⋃ (K_1 : Compacts α),
    ⋃ (_ :
      Membership.mem (γ := Set (Compacts α))
        {x : Compacts α | (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U) x} K_1),
      (↑K_1 : Set α) ⊆
  U.image (↑K : Set α)
Tactic: refine 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 α)
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 : ClusterPt x l
⊢ ⋃ (K_1 : Compacts α),
      ⋃ (_ :
        Membership.mem (γ := Set (Compacts α))
          {x : Compacts α | (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U) x} K_1),
        (↑K_1 : Set α) ⊆
    U.image (↑K : Set α)
have h : ∀ (i : Compacts α)
  (j :
    Membership.mem (γ := Set (Compacts α))
      {x : Compacts α | (fun (K' : Compacts α) ↦ ((↑K : Set α), (↑K' : Set α)) ∈ hausdorffEntourage U) x} i),
  (↑i : Set α) ⊆ U.image (↑K : Set α)
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 γ
K : NonemptyCompacts α
⊢ 𝓝 K = 𝓝 K
have simp_rw : Eq (α := Filter (NonemptyCompacts α)) (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 α
⊢ CompleteSpace.{u_1} (NonemptyCompacts α) ↔ CompleteSpace α
have refine : CompleteSpace.{u_1} (NonemptyCompacts α) → ∀ {f : Filter α} (hf : Cauchy f), ∃ (x : α), f ≤ 𝓝 x
Tactic: refine ⟨fun _ => ⟨fun {f} hf => ?_⟩, fun _ => inferInstance⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompleteSpace.{u_1} (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
⊢ ∃ (x : α), f ≤ 𝓝 x
have obtain : ∀ (K : NonemptyCompacts α) (hK : Filter.map (fun (x : α) ↦ {x}) f ≤ 𝓝 K), ∃ (x : α), f ≤ 𝓝 x
Tactic: obtain ⟨K, hK⟩ := CompleteSpace.complete <| hf.map uniformContinuous_singleton
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompleteSpace.{u_1} (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun (x : α) ↦ {x}) f ≤ 𝓝 K
⊢ ∃ (x : α), f ≤ 𝓝 x
have obtain : ∀ (x : α) (hx : x ∈ (↑K : Set α)), ∃ (x : α), f ≤ 𝓝 x
Tactic: obtain ⟨x, hx⟩ := K.nonempty
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompleteSpace.{u_1} (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun (x : α) ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ (↑K : Set α)
⊢ ∃ (x : α), f ≤ 𝓝 x
have exists : f ≤ 𝓝 x
Tactic: exists x
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompleteSpace.{u_1} (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun (x : α) ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ (↑K : Set α)
⊢ f ≤ 𝓝 x
have rw : ∀ (i' : Set α), x ∈ i' ∧ IsOpen[inst.toTopologicalSpace] i' → i' ∈ f
Tactic: rw [(nhds_basis_opens x).ge_iff]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompleteSpace.{u_1} (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun (x : α) ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ (↑K : Set α)
U : Set α
⊢ x ∈ U ∧ IsOpen[inst.toTopologicalSpace] U → U ∈ f
have this : ∀ (hxU : x ∈ U) (hU : IsOpen[inst.toTopologicalSpace] U), U ∈ f
Tactic: ⟨hxU, hU⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Closeds (goal)
Goal:
α : Type u_1
inst : UniformSpace α
h : CompleteSpace.{u_1} (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
K : NonemptyCompacts α
hK : Filter.map (fun (x : α) ↦ {x}) f ≤ 𝓝 K
x : α
hx : x ∈ (↑K : Set α)
U : Set α
hxU : x ∈ U
hU : IsOpen[inst.toTopologicalSpace] U
⊢ U ∈ f
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
      (Set.preimage (β := NonemptyCompacts α) (fun (x : α) ↦ {x})
        {K : NonemptyCompacts α | ((↑K : Set α) ∩ U).Nonempty})
      a →
    a ∈ U
Tactic: filter_upwards [hK <| (isOpen_inter_nonempty_of_isOpen hU).mem_nhds ⟨x, hx, hxU⟩]
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ (i : ι), U i
x : α
hx : x ∈ K
⊢ ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
have obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
Tactic: obtain ⟨i, hi⟩ := mem_iUnion.1 (hcover hx)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ (i : ι), U i
x : α
hx : x ∈ K
i : ι
hi : x ∈ U i
⊢ ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
have hi₁ : Membership.mem (γ := Filter α) (Filter.comap (Prod.mk x) ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s)) (U i)
Tactic: rw [← (hopen i).mem_nhds_iff, nhds_eq_comap_uniformity, ← lift'_comp_uniformity] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ (i : ι), U i
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i
have this : ∀ x ∈ K, ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
Tactic: have : ∀ x ∈ K, ∃ i, ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i := fun x hx ↦ by
    obtain ⟨i, hi⟩ := mem_iUnion.1 (hcover hx)
    rw [← (hopen i).mem_nhds_iff, nhds_eq_comap_uniformity, ← lift'_comp_uniformity] at hi
    exact ⟨i, (((basis_sets _).lift' <| monotone_id.relComp monotone_id).comap _).mem_iff.1 hi⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ (i : ι), U i
this : ∀ x ∈ K, ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i
have choose : ∀ (ind : (x : α) → x ∈ K → ι) (W : (x : α) → x ∈ K → Set (α × α)) (hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α)
  (hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)), ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i
Tactic: choose ind W hW hWU using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ (i : ι), U i
ind : (x : α) → x ∈ K → ι
W : (x : α) → x ∈ K → Set (α × α)
hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α
hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i
have rcases : ∀ (t : Finset (↑K : Type ua)) (ht : K ⊆ ⋃ x ∈ t, ball (↑x : α) (W (↑x : α) sorry)),
  ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i
Tactic: rcases hK.elim_nhds_subcover' (fun x hx ↦ ball x (W x hx)) (fun x hx ↦ ball_mem_nhds _ (hW x hx))
    with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ (i : ι), U i
ind : (x : α) → x ∈ K → ι
W : (x : α) → x ∈ K → Set (α × α)
hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α
hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)
t : Finset (↑K : Type ua)
ht : K ⊆ ⋃ x ∈ t, ball (↑x : α) (W (↑x : α) ⋯)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i
have refine : ∀ (x : α) (hx : x ∈ K), ∃ (i : ι), ball x (⋂ x ∈ t, W (↑x : α) sorry) ⊆ U i
Tactic: refine ⟨⋂ x ∈ t, W x x.2, (biInter_finset_mem _).2 fun x _ ↦ hW x x.2, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι : Sort u_2
U : ι → Set α
hK : IsCompact K
hopen : ∀ (i : ι), IsOpen[inst.toTopologicalSpace] (U i)
hcover : K ⊆ ⋃ (i : ι), U i
ind : (x : α) → x ∈ K → ι
W : (x : α) → x ∈ K → Set (α × α)
hW : ∀ (x : α) (a : x ∈ K), W x a ∈ 𝓤 α
hWU : ∀ (x : α) (a : x ∈ K), ball x (W x a ○ W x a) ⊆ U (ind x a)
t : Finset (↑K : Type ua)
ht : K ⊆ ⋃ x ∈ t, ball (↑x : α) (W (↑x : α) ⋯)
x : α
hx : x ∈ K
⊢ ∃ (i : ι), ball x (⋂ x ∈ t, W (↑x : α) ⋯) ⊆ U i
have rcases : ∀ (y : (↑K : Type ua)) (hyt : y ∈ t) (hxy : x ∈ ball (↑y : α) (W (↑y : α) sorry)),
  ∃ (i : ι), ball x (⋂ x ∈ t, W (↑x : α) sorry) ⊆ U i
Tactic: rcases mem_iUnion₂.1 (ht hx) with ⟨y, hyt, hxy⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
U : (x : α) → x ∈ K → Set α
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝 x
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x V ⊆ U (↑y : α) ⋯
have rcases : ∀ (V : Set (α × α)) (V_uni : V ∈ 𝓤 α) (hV : ∀ x ∈ K, ∃ (i : (↑K : Type ua)), ball x V ⊆ interior (U (↑i : α) sorry)),
  ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x V ⊆ U (↑y : α) sorry
Tactic: rcases lebesgue_number_lemma (U := fun x : K => interior (U x x.2)) hK (fun _ => isOpen_interior)
    (fun x hx => mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with ⟨V, V_uni, hV⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : α), ball x V ⊆ U y
have rcases : ∀ (V : Set (α × α)) (V_uni : V ∈ 𝓤 α) (hV : ∀ x ∈ K, ∃ (i : α), ball x V ⊆ interior (U i)),
  ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : α), ball x V ⊆ U y
Tactic: rcases lebesgue_number_lemma (U := fun x => interior (U x)) hK (fun _ => isOpen_interior)
    (fun x hx => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x hx)⟩) with ⟨V, V_uni, hV⟩
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι' : Sort u_2
ι : Sort u_3
p : ι' → Prop
V : ι' → Set (α × α)
U : ι → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hopen : ∀ (j : ι), IsOpen[inst.toTopologicalSpace] (U j)
hcover : K ⊆ ⋃ (j : ι), U j
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (j : ι), ball x (V i) ⊆ U j
have refine : ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (i : ι), ball x t ⊆ U i) → ∀ x ∈ K, ∃ (i : ι), ball x s ⊆ U i
Tactic: refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma hK hopen hcover)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : (x : α) → x ∈ K → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝 x
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x (V i) ⊆ U (↑y : α) ⋯
have refine : ∀ ⦃s t : Set (α × α)⦄,
  s ⊆ t →
    (∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x t ⊆ U (↑y : α) sorry) →
      ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x s ⊆ U (↑y : α) sorry
Tactic: refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhds' hK hU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : α → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : α), ball x (V i) ⊆ U y
have refine : ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (y : α), ball x t ⊆ U y) → ∀ x ∈ K, ∃ (y : α), ball x s ⊆ U y
Tactic: refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhds hK hU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : (x : α) → x ∈ K → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝[K] x
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x (V i) ∩ K ⊆ U (↑y : α) ⋯
have refine : ∀ ⦃s t : Set (α × α)⦄,
  s ⊆ t →
    (∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x t ∩ K ⊆ U (↑y : α) sorry) →
      ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x s ∩ K ⊆ U (↑y : α) sorry
Tactic: refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin' hK hU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (goal)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
ι' : Sort u_2
p : ι' → Prop
V : ι' → Set (α × α)
U : α → Set α
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝[K] x
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : α), ball x (V i) ∩ K ⊆ U y
have refine : ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (y : α), ball x t ∩ K ⊆ U y) → ∀ x ∈ K, ∃ (y : α), ball x s ∩ K ⊆ U y
Tactic: refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin hK hU)
-- Lean 4 proof step from Mathlib.Topology.UniformSpace.Compact (hypothesis)
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen[inst.toTopologicalSpace] s
hcover : K ⊆ ⋃₀ S
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s
have hcover₁ : K ⊆ ⋃ (i : (↑S : Type ua)), (↑i : Set α)
Tactic: rw [sUnion_eq_iUnion] at hcover
Cleared hypotheses: hcover