awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Compact
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
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (y : α), ball x t ⊆ U y) → ∀ x ∈ K, ∃ (y : α), ball x s ⊆ U y

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp fun y hy ↦ Subset.trans (ball_mono hst _) hy
-- Module: Mathlib.Topology.UniformSpace.Compact
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 : α) ⋯

Tactic:
(hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin' hK hU)

Premises used: Filter.HasBasis.exists_iff, Iff.mp, lebesgue_number_lemma_nhdsWithin'
-- Module: Mathlib.Topology.UniformSpace.Compact
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
refine :
  ∀ ⦃s t : Set (α × α)⦄,
    s ⊆ t →
      (∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x t ∩ K ⊆ U (↑y : α) ⋯) →
        ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x s ∩ K ⊆ U (↑y : α) ⋯
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x (V i) ∩ K ⊆ U (↑y : α) ⋯

Tactic:
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin' hK hU)

Premises used: Filter.HasBasis.exists_iff, Iff.mp, lebesgue_number_lemma_nhdsWithin'
-- Module: Mathlib.Topology.UniformSpace.Compact
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
⊢ ∀ ⦃s t : Set (α × α)⦄,
    s ⊆ t →
      (∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x t ∩ K ⊆ U (↑y : α) ⋯) →
        ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x s ∩ K ⊆ U (↑y : α) ⋯

Tactic:
fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy

Premises used: Set.Subset.trans, UniformSpace.ball_mono, Exists.imp, Set.inter_subset_inter_left
-- Module: Mathlib.Topology.UniformSpace.Compact
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
⊢ ∀ ⦃s t : Set (α × α)⦄,
    s ⊆ t →
      (∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x t ∩ K ⊆ U (↑y : α) ⋯) →
        ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x s ∩ K ⊆ U (↑y : α) ⋯

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy
-- Module: Mathlib.Topology.UniformSpace.Compact
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

Tactic:
(hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin hK hU)

Premises used: lebesgue_number_lemma_nhdsWithin, Filter.HasBasis.exists_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Compact
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
refine :
  ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (y : α), ball x t ∩ K ⊆ U y) → ∀ x ∈ K, ∃ (y : α), ball x s ∩ K ⊆ U y
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : α), ball x (V i) ∩ K ⊆ U y

Tactic:
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma_nhdsWithin hK hU)

Premises used: lebesgue_number_lemma_nhdsWithin, Filter.HasBasis.exists_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Compact
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
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (y : α), ball x t ∩ K ⊆ U y) → ∀ x ∈ K, ∃ (y : α), ball x s ∩ K ⊆ U y

Tactic:
fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy

Premises used: Set.Subset.trans, UniformSpace.ball_mono, Exists.imp, Set.inter_subset_inter_left
-- Module: Mathlib.Topology.UniformSpace.Compact
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
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (y : α), ball x t ∩ K ⊆ U y) → ∀ x ∈ K, ∃ (y : α), ball x s ∩ K ⊆ U y

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp
    fun y hy ↦ Subset.trans (Set.inter_subset_inter_left K (ball_mono hst _)) hy
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen[inst.toTopologicalSpace] s
hcover : K ⊆ ⋃₀ S
⊢ K ⊆ ⋃ (i : (↑S : Type ua)), (↑i : Set α)

Tactic:
rw [sUnion_eq_iUnion] at hcover

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen[inst.toTopologicalSpace] s
hcover : K ⊆ ⋃ (i : (↑S : Type ua)), (↑i : Set α)
⊢ ∀ (i : (↑S : Type ua)), IsOpen[inst.toTopologicalSpace] (↑i : Set α)

Tactic:
simpa
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen[inst.toTopologicalSpace] s
hcover : K ⊆ ⋃ (i : (↑S : Type ua)), (↑i : Set α)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s

Tactic:
simpa using lebesgue_number_lemma hK (by simpa) hcover

Premises used: lebesgue_number_lemma
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
mp : U ∈ 𝓝ˢ K → ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
mpr : (∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U) → U ∈ 𝓝ˢ K
⊢ U ∈ 𝓝ˢ K ↔ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
constructor
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
⊢ K ⊆ ⋃ (x : Unit), interior U

Tactic:
simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H

Premises used: Set.iUnion_const, subset_interior_iff_mem_nhdsSet
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
⊢ K ⊆ ⋃ (x : Unit), interior U

Tactic:
have HKU : K ⊆ ⋃ _ : Unit, interior U := by
        simpa only [iUnion_const, subset_interior_iff_mem_nhdsSet] using H
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ (x : Unit), interior U
⊢ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U

Tactic:
simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU

Premises used: isOpen_interior, Filter.HasBasis.lebesgue_number_lemma
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ (x : Unit), interior U
mp : ∀ (i : ι) (hpi : p i) (hi : ⋃ x ∈ K, ball x (V i) ⊆ interior U), ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U
⊢ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
obtain ⟨i, hpi, hi⟩ : ∃ i, p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ interior U := by
        simpa using hbasis.lebesgue_number_lemma hK (fun _ ↦ isOpen_interior) HKU

Premises used: interior
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ (x : Unit), interior U
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ interior U
⊢ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
⟨i, hpi, hi.trans interior_subset⟩

Premises used: interior_subset, HasSubset.Subset.trans, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
H : U ∈ 𝓝ˢ K
HKU : K ⊆ ⋃ (x : Unit), interior U
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ interior U
⊢ ∃ (i : ι), p i ∧ ⋃ x ∈ K, ball x (V i) ⊆ U

Tactic:
exact ⟨i, hpi, hi.trans interior_subset⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
⊢ U ∈ 𝓝ˢ K

Tactic:
mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi

Premises used: bUnion_mem_nhdsSet, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
mpr : ∀ x ∈ K, ball x (V i) ∈ 𝓝 x
⊢ U ∈ 𝓝ˢ K

Tactic:
refine mem_of_superset (bUnion_mem_nhdsSet fun x _ ↦ ?_) hi

Premises used: bUnion_mem_nhdsSet, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
x : α
h : x ∈ K
⊢ ball x (V i) ∈ 𝓝 x

Tactic:
ball_mem_nhds _ <| hbasis.mem_of_mem hpi

Premises used: UniformSpace.ball_mem_nhds, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
K : Set α
p : ι → Prop
V : ι → Set (α × α)
hbasis : (𝓤 α).HasBasis p V
hK : IsCompact K
U : Set α
i : ι
hpi : p i
hi : ⋃ x ∈ K, ball x (V i) ⊆ U
x : α
h : x ∈ K
⊢ ball x (V i) ∈ 𝓝 x

Tactic:
exact ball_mem_nhds _ <| hbasis.mem_of_mem hpi

Premises used: UniformSpace.ball_mem_nhds, Filter.HasBasis.mem_of_mem
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
⊢ Bᶜ ∈ 𝓝ˢ A

Tactic:
have : Bᶜ ∈ 𝓝ˢ A := hB.isOpen_compl.mem_nhdsSet.mpr h.le_compl_right
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
this : Bᶜ ∈ 𝓝ˢ A
⊢ ∃ i ∈ 𝓤 α, ⋃ x ∈ A, ball x (id i) ⊆ Bᶜ

Tactic:
rw [(hA.nhdsSet_basis_uniformity (Filter.basis_sets _)).mem_iff] at this

Premises used: Filter.HasBasis.mem_iff, Filter.basis_sets, IsCompact.nhdsSet_basis_uniformity
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
this : ∃ i ∈ 𝓤 α, ⋃ x ∈ A, ball x (id i) ⊆ Bᶜ
rcases :
  ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α) (hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ),
    ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)

Tactic:
rcases this with ⟨U, hU, hUAB⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
rcases :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVsymm : SetRel.IsSymm V) (hVU : V ○ V ⊆ U),
    ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)

Tactic:
rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩

Premises used: comp_symm_mem_uniformity_sets
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)

Tactic:
⟨V, hV, Set.disjoint_left.mpr fun x => ?_⟩

Premises used: Iff.mpr, Set.disjoint_left, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
refine : ∀ (x : α), Membership.mem (γ := Set α) (⋃ x ∈ A, ball x V) x → x ∉ ⋃ x ∈ B, ball x V
⊢ ∃ V ∈ 𝓤 α, Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)

Tactic:
refine ⟨V, hV, Set.disjoint_left.mpr fun x => ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x : α
simp : (∃ (i : α) (_ : i ∈ A), x ∈ ball i V) → ¬∃ (i : α) (_ : i ∈ B), x ∈ ball i V
⊢ Membership.mem (γ := Set α) (⋃ x ∈ A, ball x V) x → x ∉ ⋃ x ∈ B, ball x V

Tactic:
simp only [mem_iUnion₂]

Premises used: Set.mem_iUnion₂
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : x ∈ ball a V
b : α
hb : b ∈ B
hxb : x ∈ ball b V
rw : ∀ (hxa : a ∈ ball x V) (b : α) (hb : b ∈ B) (hxb : b ∈ ball x V), False
⊢ False

Tactic:
rw [mem_ball_symmetry] at hxa hxb

Premises used: UniformSpace.mem_ball_symmetry
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : a ∈ ball x V
b : α
hb : b ∈ B
hxb : b ∈ ball x V
⊢ False

Tactic:
hUAB (mem_iUnion₂_of_mem ha <| hVU <| mem_comp_of_mem_ball hxa hxb) hb

Premises used: UniformSpace.mem_comp_of_mem_ball, Set.mem_iUnion₂_of_mem
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
U : Set (α × α)
hU : U ∈ 𝓤 α
hUAB : ⋃ x ∈ A, ball x (id U) ⊆ Bᶜ
V : Set (α × α)
hV : V ∈ 𝓤 α
hVsymm : SetRel.IsSymm V
hVU : V ○ V ⊆ U
x a : α
ha : a ∈ A
hxa : a ∈ ball x V
b : α
hb : b ∈ B
hxb : b ∈ ball x V
⊢ False

Tactic:
exact hUAB (mem_iUnion₂_of_mem ha <| hVU <| mem_comp_of_mem_ball hxa hxb) hb

Premises used: UniformSpace.mem_comp_of_mem_ball, Set.mem_iUnion₂_of_mem
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
rcases :
  ∀ (V : Set (α × α)) (hV : V ∈ 𝓤 α) (hVAB : Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)),
    ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
⊢ ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
rcases h.exists_uniform_thickening hA hB with ⟨V, hV, hVAB⟩

Premises used: Disjoint.exists_uniform_thickening
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
rcases :
  ∀ (i : ι) (hi : p i) (hiV : s i ⊆ V),
    ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))
⊢ ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
rcases hU.mem_iff.1 hV with ⟨i, hi, hiV⟩

Premises used: Filter.HasBasis.mem_iff, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
i : ι
hi : p i
hiV : s i ⊆ V
⊢ ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
⟨i, hi, hVAB.mono (iUnion₂_mono fun a _ => ball_mono hiV a)
    (iUnion₂_mono fun b _ => ball_mono hiV b)⟩

Premises used: UniformSpace.ball_mono, Set.iUnion₂_mono, And.intro, Exists.intro, Disjoint.mono
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
ι : Sort u_1
inst : UniformSpace α
p : ι → Prop
s : ι → Set (α × α)
hU : (𝓤 α).HasBasis p s
A B : Set α
hA : IsCompact A
hB : IsClosed[inst.toTopologicalSpace] B
h : Disjoint A B
V : Set (α × α)
hV : V ∈ 𝓤 α
hVAB : Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x V) (⋃ x ∈ B, ball x V)
i : ι
hi : p i
hiV : s i ⊆ V
⊢ ∃ (i : ι), p i ∧ Disjoint.{ua} (α := Set α) (⋃ x ∈ A, ball x (s i)) (⋃ x ∈ B, ball x (s i))

Tactic:
exact ⟨i, hi, hVAB.mono (iUnion₂_mono fun a _ => ball_mono hiV a)
    (iUnion₂_mono fun b _ => ball_mono hiV b)⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K U : Set α
hK : IsCompact K
hU : IsOpen[inst.toTopologicalSpace] U
hKU : K ⊆ U
⊢ ∃ V ∈ 𝓤 α, IsOpen[instTopologicalSpaceProd] V ∧ ∀ x ∈ K, ball x V ⊆ U

Tactic:
let ⟨V, ⟨hV, hVo⟩, hVU⟩ :=
    (hK.nhdsSet_basis_uniformity uniformity_hasBasis_open).mem_iff.1 (hU.mem_nhdsSet.2 hKU)
  ⟨V, hV, hVo, iUnion₂_subset_iff.1 hVU⟩

Premises used: Iff.mpr, Filter.HasBasis.mem_iff, uniformity, Membership.mem, Exists, And, _private.0.lebesgue_number_of_compact_open.match_1, And.intro, Exists.intro, Iff.mp, IsOpen, Set.iUnion₂_subset_iff, IsCompact.nhdsSet_basis_uniformity, uniformity_hasBasis_open, IsOpen.mem_nhdsSet
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
⊢ 𝓝ˢ (diagonal α) = 𝓤 α

Tactic:
nhdsSet_diagonal_le_uniformity.antisymm ?_

Premises used: LE.le.antisymm, nhdsSet_diagonal_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
refine : 𝓤 α ≤ 𝓝ˢ (diagonal α)
⊢ 𝓝ˢ (diagonal α) = 𝓤 α

Tactic:
refine nhdsSet_diagonal_le_uniformity.antisymm ?_

Premises used: LE.le.antisymm, nhdsSet_diagonal_le_uniformity
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
rw :
  HasBasis (α := (α × α) × α × α)
    (Filter.comap (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α))
    (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
⊢ HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U

Tactic:
rw [uniformity_prod_eq_comap_prod]

Premises used: uniformity_prod_eq_comap_prod
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
⊢ HasBasis (α := (α × α) × α × α)
    (Filter.comap (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α))
    (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U

Tactic:
(𝓤 α).basis_sets.prod_self.comap _

Premises used: Filter.HasBasis.prod_self, uniformity, Filter.HasBasis.comap, Filter.basis_sets
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
⊢ HasBasis (α := (α × α) × α × α)
    (Filter.comap (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 α))
    (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U

Tactic:
exact (𝓤 α).basis_sets.prod_self.comap _

Premises used: Filter.HasBasis.prod_self, uniformity, Filter.HasBasis.comap, Filter.basis_sets
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
⊢ HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U

Tactic:
have :
    (𝓤 (α × α)).HasBasis (fun U => U ∈ 𝓤 α) fun U =>
      (fun p : (α × α) × α × α => ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U := by
    rw [uniformity_prod_eq_comap_prod]
    exact (𝓤 α).basis_sets.prod_self.comap _
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
this :
  HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)

Tactic:
(isCompact_diagonal.nhdsSet_basis_uniformity this).ge_iff.2 fun U hU => ?_

Premises used: Iff.mpr, Set.Mem, setOf, isCompact_diagonal, Filter.HasBasis.ge_iff, IsCompact.nhdsSet_basis_uniformity
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
this :
  HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
refine :
  ∀ (U : Set (α × α)) (hU : U ∈ 𝓤 α),
    ⋃ x ∈ diagonal α, ball x ((fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U) ∈ 𝓤 α
⊢ 𝓤 α ≤ 𝓝ˢ (diagonal α)

Tactic:
refine (isCompact_diagonal.nhdsSet_basis_uniformity this).ge_iff.2 fun U hU => ?_

Premises used: Iff.mpr, isCompact_diagonal, Filter.HasBasis.ge_iff, IsCompact.nhdsSet_basis_uniformity
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
this :
  HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ diagonal α, ball x ((fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U) ∈ 𝓤 α

Tactic:
mem_of_superset hU fun ⟨x, y⟩ hxy => mem_iUnion₂.2
    ⟨(x, x), rfl, refl_mem_uniformity hU, hxy⟩

Premises used: Iff.mpr, SProd.sprod, refl_mem_uniformity, Membership.mem, Prod.mk, Set.mem_iUnion₂, Prod.fst, UniformSpace.ball, Set.preimage, And.intro, _private.0.nhdsSet_diagonal_eq_uniformity.match_1, Exists.intro, Prod.snd, Set.iUnion, rfl, Filter.mem_of_superset
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
inst_1 : CompactSpace α
this :
  HasBasis (α := (α × α) × α × α) (𝓤 (α × α)) (fun (U : Set (α × α)) ↦ U ∈ 𝓤 α) fun (U : Set (α × α)) ↦
    (fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U
U : Set (α × α)
hU : U ∈ 𝓤 α
⊢ ⋃ x ∈ diagonal α, ball x ((fun (p : (α × α) × α × α) ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) ⁻¹' U ×ˢ U) ∈ 𝓤 α

Tactic:
exact mem_of_superset hU fun ⟨x, y⟩ hxy => mem_iUnion₂.2
    ⟨(x, x), rfl, refl_mem_uniformity hU, hxy⟩