awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
inst : UniformSpace α
inst_1 : UniformSpace β
f : α → β
hf : IsUniformInducing f
⊢ IsUniformInducing (NonemptyCompacts.map f ⋯)

Tactic:
.of_comp hf.uniformContinuous.nonemptyCompacts_map uniformContinuous_coe <|
    hf.image_hausdorff.comp isUniformEmbedding_coe.isUniformInducing

Premises used: TopologicalSpace.NonemptyCompacts.uniformContinuous_coe, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe, IsUniformEmbedding.isUniformInducing, IsUniformInducing.of_comp, IsUniformInducing.comp, UniformContinuous.nonemptyCompacts_map, IsUniformInducing.image_hausdorff, IsUniformInducing.uniformContinuous
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : DiscreteUniformity α
⊢ DiscreteUniformity.{u_1} (NonemptyCompacts α)

Tactic:
isUniformEmbedding_coe.discreteUniformity

Premises used: TopologicalSpace.NonemptyCompacts.isUniformEmbedding_coe, IsUniformEmbedding.discreteUniformity
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ DiscreteUniformity.{u_1} (NonemptyCompacts α) ↔ DiscreteUniformity α

Tactic:
⟨fun _ => isUniformEmbedding_singleton.discreteUniformity, fun _ => inferInstance⟩

Premises used: inferInstance, IsUniformEmbedding.discreteUniformity, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_singleton, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : UniformSpace α
inst_1 : UniformSpace β
inst_2 : UniformSpace γ
inst_3 : CompleteSpace α
⊢ CompleteSpace.{u_1} (NonemptyCompacts α)

Tactic:
isUniformEmbedding_toCompacts.completeSpace isClosedEmbedding_toCompacts.isClosed_range.isComplete

Premises used: IsUniformEmbedding.toIsUniformInducing, IsUniformInducing.completeSpace, TopologicalSpace.NonemptyCompacts.isUniformEmbedding_toCompacts, IsClosed.isComplete
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
⊢ CompleteSpace.{u_1} (NonemptyCompacts α) ↔ CompleteSpace α

Tactic:
⟨fun _ => ⟨fun {f} hf => ?_⟩, fun _ => inferInstance⟩

Premises used: inferInstance, CompleteSpace.mk, Iff.intro
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
refine : CompleteSpace.{u_1} (NonemptyCompacts α) → ∀ {f : Filter α} (hf : Cauchy f), ∃ (x : α), f ≤ 𝓝 x
⊢ CompleteSpace.{u_1} (NonemptyCompacts α) ↔ CompleteSpace α

Tactic:
refine ⟨fun _ => ⟨fun {f} hf => ?_⟩, fun _ => inferInstance⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h : CompleteSpace.{u_1} (NonemptyCompacts α)
f : Filter α
hf : Cauchy f
obtain : ∀ (K : NonemptyCompacts α) (hK : Filter.map (fun (x : α) ↦ {x}) f ≤ 𝓝 K), ∃ (x : α), f ≤ 𝓝 x
⊢ ∃ (x : α), f ≤ 𝓝 x

Tactic:
obtain ⟨K, hK⟩ := CompleteSpace.complete <| hf.map uniformContinuous_singleton

Premises used: Cauchy.map, TopologicalSpace.NonemptyCompacts.uniformContinuous_singleton, CompleteSpace.complete
-- Module: Mathlib.Topology.UniformSpace.Closeds
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
obtain : ∀ (x : α) (hx : x ∈ (↑K : Set α)), ∃ (x : α), f ≤ 𝓝 x
⊢ ∃ (x : α), f ≤ 𝓝 x

Tactic:
obtain ⟨x, hx⟩ := K.nonempty

Premises used: TopologicalSpace.NonemptyCompacts.nonempty
-- Module: Mathlib.Topology.UniformSpace.Closeds
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 α)
exists : f ≤ 𝓝 x
⊢ ∃ (x : α), f ≤ 𝓝 x

Tactic:
exists x
-- Module: Mathlib.Topology.UniformSpace.Closeds
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 α)
rw : ∀ (i' : Set α), x ∈ i' ∧ IsOpen[inst.toTopologicalSpace] i' → i' ∈ f
⊢ f ≤ 𝓝 x

Tactic:
rw [(nhds_basis_opens x).ge_iff]

Premises used: Filter.HasBasis.ge_iff, nhds_basis_opens
-- Module: Mathlib.Topology.UniformSpace.Closeds
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 α
this : ∀ (hxU : x ∈ U) (hU : IsOpen[inst.toTopologicalSpace] U), U ∈ f
⊢ x ∈ U ∧ IsOpen[inst.toTopologicalSpace] U → U ∈ f

Tactic:
⟨hxU, hU⟩
-- Module: Mathlib.Topology.UniformSpace.Closeds
Goal:
α : Type u_1
inst : UniformSpace α
h_1 : 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
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
        (Set.preimage (β := NonemptyCompacts α) (fun (x : α) ↦ {x})
          {K : NonemptyCompacts α | ((↑K : Set α) ∩ U).Nonempty})
        a →
      a ∈ U
⊢ U ∈ f

Tactic:
filter_upwards [hK <| (isOpen_inter_nonempty_of_isOpen hU).mem_nhds ⟨x, hx, hxU⟩]

Premises used: TopologicalSpace.NonemptyCompacts.isOpen_inter_nonempty_of_isOpen, And.intro, IsOpen.mem_nhds, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Closeds
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
⊢ ∀ (a : α),
    Membership.mem (γ := Set α)
        (Set.preimage (β := NonemptyCompacts α) (fun (x : α) ↦ {x})
          {K : NonemptyCompacts α | ((↑K : Set α) ∩ U).Nonempty})
        a →
      a ∈ U

Tactic:
simp
-- Module: Mathlib.Topology.UniformSpace.Compact
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
obtain : ∀ (i : ι) (hi : x ∈ U i), ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i
⊢ ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i

Tactic:
obtain ⟨i, hi⟩ := mem_iUnion.1 (hcover hx)

Premises used: Set.mem_iUnion, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Compact
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
⊢ 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

Premises used: lift'_comp_uniformity, IsOpen.mem_nhds_iff, nhds_eq_comap_uniformity
-- Module: Mathlib.Topology.UniformSpace.Compact
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 : Membership.mem (γ := Filter α) (Filter.comap (Prod.mk x) ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s)) (U i)
⊢ ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i

Tactic:
⟨i, (((basis_sets _).lift' <| monotone_id.relComp monotone_id).comap _).mem_iff.1 hi⟩

Premises used: Filter.HasBasis.mem_iff, monotone_id, Monotone.relComp, Filter.HasBasis.comap, Filter.basis_sets, Exists.intro, Iff.mp, Filter.HasBasis.lift'
-- Module: Mathlib.Topology.UniformSpace.Compact
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 : Membership.mem (γ := Filter α) (Filter.comap (Prod.mk x) ((𝓤 α).lift' fun (s : SetRel α α) ↦ s ○ s)) (U i)
⊢ ∃ (i : ι), ∃ V ∈ 𝓤 α, ball x (V ○ V) ⊆ U i

Tactic:
exact ⟨i, (((basis_sets _).lift' <| monotone_id.relComp monotone_id).comap _).mem_iff.1 hi⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
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 ∈ 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⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
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
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
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i

Tactic:
choose ind W hW hWU using this
-- Module: Mathlib.Topology.UniformSpace.Compact
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)
rcases :
  ∀ (t : Finset (↑K : Type ua)) (ht : K ⊆ ⋃ x ∈ t, ball (↑x : α) (W (↑x : α) ⋯)),
    ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i
⊢ ∃ 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⟩

Premises used: UniformSpace.ball_mem_nhds, UniformSpace.ball, IsCompact.elim_nhds_subcover'
-- Module: Mathlib.Topology.UniformSpace.Compact
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

Tactic:
⟨⋂ x ∈ t, W x x.2, (biInter_finset_mem _).2 fun x _ ↦ hW x x.2, fun x hx ↦ ?_⟩

Premises used: Iff.mpr, Set.iInter, Filter.biInter_finset_mem, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Compact
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 : α) ⋯)
refine : ∀ (x : α) (hx : x ∈ K), ∃ (i : ι), ball x (⋂ x ∈ t, W (↑x : α) ⋯) ⊆ U i
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (i : ι), ball x V ⊆ U i

Tactic:
refine ⟨⋂ x ∈ t, W x x.2, (biInter_finset_mem _).2 fun x _ ↦ hW x x.2, fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
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
rcases :
  ∀ (y : (↑K : Type ua)) (hyt : y ∈ t) (hxy : x ∈ ball (↑y : α) (W (↑y : α) ⋯)),
    ∃ (i : ι), ball x (⋂ x ∈ t, W (↑x : α) ⋯) ⊆ U i
⊢ ∃ (i : ι), ball x (⋂ x ∈ t, W (↑x : α) ⋯) ⊆ U i

Tactic:
rcases mem_iUnion₂.1 (ht hx) with ⟨y, hyt, hxy⟩

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.UniformSpace.Compact
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
y : (↑K : Type ua)
hyt : y ∈ t
hxy : x ∈ ball (↑y : α) (W (↑y : α) ⋯)
⊢ ∃ (i : ι), ball x (⋂ x ∈ t, W (↑x : α) ⋯) ⊆ U i

Tactic:
⟨ind y y.2, fun z hz ↦ hWU _ _ ⟨x, hxy, mem_iInter₂.1 hz _ hyt⟩⟩

Premises used: Set.mem_iInter₂, And.intro, Exists.intro, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.UniformSpace.Compact
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
y : (↑K : Type ua)
hyt : y ∈ t
hxy : x ∈ ball (↑y : α) (W (↑y : α) ⋯)
⊢ ∃ (i : ι), ball x (⋂ x ∈ t, W (↑x : α) ⋯) ⊆ U i

Tactic:
exact ⟨ind y y.2, fun z hz ↦ hWU _ _ ⟨x, hxy, mem_iInter₂.1 hz _ hyt⟩⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
U : (x : α) → x ∈ K → Set α
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝 x
rcases :
  ∀ (V : Set (α × α)) (V_uni : V ∈ 𝓤 α) (hV : ∀ x ∈ K, ∃ (i : (↑K : Type ua)), ball x V ⊆ interior (U (↑i : α) ⋯)),
    ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x V ⊆ U (↑y : α) ⋯
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x V ⊆ U (↑y : α) ⋯

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⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, isOpen_interior, Set.mem_iUnion, Subtype.mk, lebesgue_number_lemma, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Compact
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 : Set (α × α)
V_uni : V ∈ 𝓤 α
hV : ∀ x ∈ K, ∃ (i : (↑K : Type ua)), ball x V ⊆ interior (U (↑i : α) ⋯)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x V ⊆ U (↑y : α) ⋯

Tactic:
⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩

Premises used: Exists.imp, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Compact
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 : Set (α × α)
V_uni : V ∈ 𝓤 α
hV : ∀ x ∈ K, ∃ (i : (↑K : Type ua)), ball x V ⊆ interior (U (↑i : α) ⋯)
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x V ⊆ U (↑y : α) ⋯

Tactic:
exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
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
⊢ ∃ 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⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, isOpen_interior, Set.mem_iUnion, lebesgue_number_lemma, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
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:
⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩

Premises used: Exists.imp, And.intro, Exists.intro
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝 x
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:
exact ⟨V, V_uni, fun x hx => (hV x hx).imp fun _ hy => hy.trans interior_subset⟩
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
U : (x : α) → x ∈ K → Set α
hK : IsCompact K
hU : ∀ (x : α) (hx : x ∈ K), U x hx ∈ 𝓝[K] x
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x V ∩ K ⊆ U (↑y : α) ⋯

Tactic:
(lebesgue_number_lemma_nhds' hK (fun x hx => Filter.mem_inf_principal'.1 (hU x hx))).imp
    fun _ ⟨V_uni, hV⟩ => ⟨V_uni, fun x hx => (hV x hx).imp fun _ hy => (inter_subset _ _ _).2 hy⟩

Premises used: Exists.imp, lebesgue_number_lemma_nhds', Iff.mp, Filter.mem_inf_principal'
-- Module: Mathlib.Topology.UniformSpace.Compact
Goal:
α : Type ua
inst : UniformSpace α
K : Set α
U : α → Set α
hK : IsCompact K
hU : ∀ x ∈ K, U x ∈ 𝓝[K] x
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ (y : α), ball x V ∩ K ⊆ U y

Tactic:
(lebesgue_number_lemma_nhds hK (fun x hx => Filter.mem_inf_principal'.1 (hU x hx))).imp
    fun _ ⟨V_uni, hV⟩ => ⟨V_uni, fun x hx => (hV x hx).imp fun _ hy => (inter_subset _ _ _).2 hy⟩

Premises used: lebesgue_number_lemma_nhds, Exists.imp, Iff.mp, Filter.mem_inf_principal'
-- Module: Mathlib.Topology.UniformSpace.Compact
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

Tactic:
(hbasis.exists_iff ?_).1 (lebesgue_number_lemma hK hopen hcover)

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

Tactic:
refine (hbasis.exists_iff ?_).1 (lebesgue_number_lemma hK hopen hcover)

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

Tactic:
fun s t hst ht x hx ↦ (ht x hx).imp fun i hi ↦ Subset.trans (ball_mono hst _) hi

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

Tactic:
exact fun s t hst ht x hx ↦ (ht x hx).imp fun i hi ↦ Subset.trans (ball_mono hst _) hi
-- 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 ∈ 𝓝 x
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : (↑K : Type ua)), ball x (V i) ⊆ U (↑y : α) ⋯

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

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

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

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

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

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

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

Premises used: lebesgue_number_lemma_nhds, 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 ∈ 𝓝 x
refine : ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (y : α), ball x t ⊆ U y) → ∀ x ∈ K, ∃ (y : α), ball x s ⊆ U y
⊢ ∃ (i : ι'), p i ∧ ∀ x ∈ K, ∃ (y : α), ball x (V i) ⊆ U y

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

Premises used: lebesgue_number_lemma_nhds, 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 ∈ 𝓝 x
⊢ ∀ ⦃s t : Set (α × α)⦄, s ⊆ t → (∀ x ∈ K, ∃ (y : α), ball x t ⊆ U y) → ∀ x ∈ K, ∃ (y : α), ball x s ⊆ U y

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

Premises used: Set.Subset.trans, UniformSpace.ball_mono, Exists.imp