awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
⊢ (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot

Tactic:
haveI := hx.neBot
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
right : ClusterPt (f x) l
⊢ ∃ x ∈ f '' s, ClusterPt x l

Tactic:
use f x, mem_image_of_mem f hxs

Premises used: Set.mem_image_of_mem
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ Tendsto f (𝓝[s] x ⊓ comap f l) (𝓝 (f x) ⊓ l)

Tactic:
(hf x hxs).inf (@tendsto_comap _ _ f l)

Premises used: Filter.tendsto_comap, Filter.Tendsto.inf
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
h : 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝[s] x ⊓ comap f l
⊢ Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)

Tactic:
convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1

Premises used: Filter.tendsto_comap, Filter.Tendsto.inf
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ 𝓝 x ⊓ (comap f l ⊓ 𝓟 s) = 𝓝 x ⊓ 𝓟 s ⊓ comap f l

Tactic:
ac_rfl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
⊢ Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)

Tactic:
have : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l) := by
    convert! (hf x hxs).inf (@tendsto_comap _ _ f l) using 1
    rw [nhdsWithin]
    ac_rfl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this_2 : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
this : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)
⊢ ClusterPt (f x) l

Tactic:
this.neBot

Premises used: ClusterPt, Filter.Tendsto.neBot
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : ContinuousOn f s
l : Filter Y
lne : l.NeBot
ls : l ≤ 𝓟 (f '' s)
this_1 : (comap f l ⊓ 𝓟 s).NeBot
x : X
hxs : x ∈ s
hx : ClusterPt x (comap f l ⊓ 𝓟 s)
this_2 : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot
this : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)
⊢ ClusterPt (f x) l

Tactic:
exact this.neBot

Premises used: Filter.Tendsto.neBot
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
f : X → Y
hs : IsCompact s
hf : Continuous[inst, inst_1] f
⊢ IsCompact (f '' s)

Tactic:
hs.image_of_continuousOn hf.continuousOn

Premises used: Continuous.continuousOn, IsCompact.image_of_continuousOn
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
f : Filter X
hs : IsCompact s
hf₂ : f ≤ 𝓟 s
ht₁ : IsOpen[inst] t
ht₂ : ∀ x ∈ s, ClusterPt x f → x ∈ t
⊢ t ∈ f

Tactic:
Classical.by_cases mem_of_eq_bot fun (this : f ⊓ 𝓟 tᶜ ≠ ⊥) =>
    let ⟨x, hx, (hfx : ClusterPt x <| f ⊓ 𝓟 tᶜ)⟩ := @hs _ ⟨this⟩ <| inf_le_of_left_le hf₂
    have : x ∈ t := ht₂ x hx hfx.of_inf_left
    have : tᶜ ∩ t ∈ 𝓝[tᶜ] x := inter_mem_nhdsWithin _ (IsOpen.mem_nhds ht₁ this)
    have A : 𝓝[tᶜ] x = ⊥ := empty_mem_iff_bot.1 <| compl_inter_self t ▸ this
    have : 𝓝[tᶜ] x ≠ ⊥ := hfx.of_inf_right.ne
    absurd A this

Premises used: inter_mem_nhdsWithin, Filter.NeBot.ne, Compl.compl, _private.0.IsCompact.adherence_nhdset.match_1, Membership.mem, Eq.rec, inf_le_of_left_le, absurd, Filter.empty_mem_iff_bot, IsOpen.mem_nhds, Iff.mp, Set.compl_inter_self, Classical.by_cases, ClusterPt.of_inf_left, ClusterPt.of_inf_right, Filter.mem_of_eq_bot
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x

Tactic:
(forall_neBot_le_iff ?_).trans ?_

Premises used: Filter.forall_neBot_le_iff, Iff.trans, IsCompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
refine_1 : Monotone (β := Prop) fun (f : Filter X) ↦ ∃ x ∈ s, ClusterPt x f
refine_2 :
  (∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x (↑f : Filter X)) ↔
    ∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x

Tactic:
refine (forall_neBot_le_iff ?_).trans ?_

Premises used: Filter.forall_neBot_le_iff, Iff.trans
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f g : Filter X
hle : f ≤ g
x : X
hxs : x ∈ s
hxf : ClusterPt x f
⊢ ∃ x ∈ s, ClusterPt x g

Tactic:
⟨x, hxs, hxf.mono hle⟩

Premises used: ClusterPt.mono, And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
f g : Filter X
hle : f ≤ g
x : X
hxs : x ∈ s
hxf : ClusterPt x f
⊢ ∃ x ∈ s, ClusterPt x g

Tactic:
exact ⟨x, hxs, hxf.mono hle⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ (∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, ClusterPt x (↑f : Filter X)) ↔
    ∀ (f : Ultrafilter X), (↑f : Filter X) ≤ 𝓟 s → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x

Tactic:
simp only [Ultrafilter.clusterPt_iff]

Premises used: Ultrafilter.clusterPt_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x

Tactic:
simp only [isCompact_iff_ultrafilter_le_nhds, le_principal_iff, Ultrafilter.mem_coe]

Premises used: Filter.le_principal_iff, isCompact_iff_ultrafilter_le_nhds, Ultrafilter.mem_coe
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
⊢ l ≤ 𝓝ˢ s'

Tactic:
le_iff_ultrafilter.2 fun f hf ↦ ?_

Premises used: Iff.mpr, Filter.le_iff_ultrafilter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
refine : ∀ (f : Ultrafilter X) (hf : (↑f : Filter X) ≤ l), (↑f : Filter X) ≤ 𝓝ˢ s'
⊢ l ≤ 𝓝ˢ s'

Tactic:
refine le_iff_ultrafilter.2 fun f hf ↦ ?_

Premises used: Iff.mpr, Filter.le_iff_ultrafilter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
rcases : ∀ (x : X) (hxs : x ∈ s) (hx : (↑f : Filter X) ≤ 𝓝 x), (↑f : Filter X) ≤ 𝓝ˢ s'
⊢ (↑f : Filter X) ≤ 𝓝ˢ s'

Tactic:
rcases hs.ultrafilter_le_nhds' f (hf hmem) with ⟨x, hxs, hx⟩

Premises used: IsCompact.ultrafilter_le_nhds'
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
x : X
hxs : x ∈ s
hx : (↑f : Filter X) ≤ 𝓝 x
grw : 𝓝 x ≤ 𝓝ˢ s'
⊢ (↑f : Filter X) ≤ 𝓝ˢ s'

Tactic:
grw [hx]
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
x : X
hxs : x ∈ s
hx : (↑f : Filter X) ≤ 𝓝 x
⊢ 𝓝 x ≤ 𝓝ˢ s'

Tactic:
nhds_le_nhdsSet ?_

Premises used: nhds_le_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
x : X
hxs : x ∈ s
hx : (↑f : Filter X) ≤ 𝓝 x
refine : x ∈ s'
⊢ 𝓝 x ≤ 𝓝ˢ s'

Tactic:
refine nhds_le_nhdsSet ?_

Premises used: nhds_le_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
x : X
hxs : x ∈ s
hx : (↑f : Filter X) ≤ 𝓝 x
⊢ x ∈ s'

Tactic:
h x hxs (.mono (.of_le_nhds hx) hf)

Premises used: ClusterPt.mono, ClusterPt.of_le_nhds
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
s' : Set X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x ∈ s'
f : Ultrafilter X
hf : (↑f : Filter X) ≤ l
x : X
hxs : x ∈ s
hx : (↑f : Filter X) ≤ 𝓝 x
⊢ x ∈ s'

Tactic:
exact h x hxs (.mono (.of_le_nhds hx) hf)

Premises used: ClusterPt.mono, ClusterPt.of_le_nhds
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
rw : l ≤ 𝓝ˢ {y}
⊢ l ≤ 𝓝 y

Tactic:
rw [← nhdsSet_singleton]

Premises used: nhdsSet_singleton
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝ˢ {y}

Tactic:
hs.le_nhdsSet_of_clusterPt hmem h

Premises used: IsCompact.le_nhdsSet_of_clusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
l : Filter X
y : X
hmem : s ∈ l
h : ∀ x ∈ s, ClusterPt x l → x = y
⊢ l ≤ 𝓝ˢ {y}

Tactic:
exact hs.le_nhdsSet_of_clusterPt hmem h

Premises used: IsCompact.le_nhdsSet_of_clusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
s' : Set X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x ∈ s'
⊢ Tendsto f l (𝓝ˢ s')

Tactic:
hs.le_nhdsSet_of_clusterPt (mem_map.2 hmem) h

Premises used: Iff.mpr, IsCompact.le_nhdsSet_of_clusterPt, Filter.Tendsto, Filter.mem_map
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
rw : Tendsto f l (𝓝ˢ {y})
⊢ Tendsto f l (𝓝 y)

Tactic:
rw [← nhdsSet_singleton]

Premises used: nhdsSet_singleton
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝ˢ {y})

Tactic:
hs.tendsto_nhdsSet_of_mapClusterPt hmem h

Premises used: IsCompact.tendsto_nhdsSet_of_mapClusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
Y : Type u_2
l : Filter Y
y : X
f : Y → X
hs : IsCompact s
hmem : ∀ᶠ (x : Y) in l, f x ∈ s
h : ∀ x ∈ s, MapClusterPt x l f → x = y
⊢ Tendsto f l (𝓝ˢ {y})

Tactic:
exact hs.tendsto_nhdsSet_of_mapClusterPt hmem h

Premises used: IsCompact.tendsto_nhdsSet_of_mapClusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hι : Nonempty ι
hs : IsCompact s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
hdU : Directed (fun (x1 x2 : Set X) ↦ x1 ⊆ x2) U
⊢ ∃ (i : ι), s ⊆ U i

Tactic:
hι.elim fun i₀ =>
    IsCompact.induction_on hs ⟨i₀, empty_subset _⟩ (fun _ _ hs ⟨i, hi⟩ => ⟨i, hs.trans hi⟩)
      (fun _ _ ⟨i, hi⟩ ⟨j, hj⟩ =>
        let ⟨k, hki, hkj⟩ := hdU i j
        ⟨k, union_subset (Subset.trans hi hki) (Subset.trans hj hkj)⟩)
      fun _x hx =>
      let ⟨i, hi⟩ := mem_iUnion.1 (hsU hx)
      ⟨U i, mem_nhdsWithin_of_mem_nhds (IsOpen.mem_nhds (hUo i) hi), i, Subset.refl _⟩

Premises used: Nonempty.elim, IsCompact.induction_on
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type v
hs : IsCompact s
U : ι → Set X
hUo : ∀ (i : ι), IsOpen[inst] (U i)
hsU : s ⊆ ⋃ (i : ι), U i
⊢ ∃ (t : Finset ι), s ⊆ ⋃ i ∈ t, U i

Tactic:
hs.elim_directed_cover _ (fun _ => isOpen_biUnion fun i _ => hUo i)
    (iUnion_eq_iUnion_finset U ▸ hsU)
    (directed_of_isDirected_le fun _ _ h => biUnion_subset_biUnion_left h)

Premises used: Eq.rec, directed_of_isDirected_le, Set.iUnion_eq_iUnion_finset, Set.biUnion_subset_biUnion_left, isOpen_biUnion, IsCompact.elim_directed_cover
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
rcases :
  ∀ (t : Finset (↑s : Type u)) (hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)),
    ∃ (t : Finset (↑s : Type u)), ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝ˢ s
⊢ ∃ (t : Finset (↑s : Type u)), ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝ˢ s

Tactic:
rcases hs.elim_finite_subcover (fun x : s ↦ interior (U x x.2)) (fun _ ↦ isOpen_interior)
    fun x hx ↦ mem_iUnion.2 ⟨⟨x, hx⟩, mem_interior_iff_mem_nhds.2 <| hU _ _⟩ with ⟨t, hst⟩

Premises used: Iff.mpr, mem_interior_iff_mem_nhds, isOpen_interior, Set.mem_iUnion, Subtype.mk, IsCompact.elim_finite_subcover, interior, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
⊢ ∃ (t : Finset (↑s : Type u)), ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝ˢ s

Tactic:
⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩

Premises used: Iff.mpr, mem_nhdsSet_iff_forall, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
refine : ∀ (x : X) (hx : x ∈ s), ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝 x
⊢ ∃ (t : Finset (↑s : Type u)), ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝ˢ s

Tactic:
refine ⟨t, mem_nhdsSet_iff_forall.2 fun x hx ↦ ?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
x : X
hx : x ∈ s
rcases : ∀ (y : (↑s : Type u)) (hyt : y ∈ t) (hy : x ∈ interior (U (↑y : X) ⋯)), ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝 x
⊢ ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝 x

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

Premises used: Set.mem_iUnion₂, Iff.mp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
x : X
hx : x ∈ s
y : (↑s : Type u)
hyt : y ∈ t
hy : x ∈ interior (U (↑y : X) ⋯)
⊢ ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝 x

Tactic:
mem_of_superset ?_ (subset_biUnion_of_mem hyt)

Premises used: Set.subset_biUnion_of_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
x : X
hx : x ∈ s
y : (↑s : Type u)
hyt : y ∈ t
hy : x ∈ interior (U (↑y : X) ⋯)
refine : U (↑y : X) ⋯ ∈ 𝓝 x
⊢ ⋃ x ∈ t, U (↑x : X) ⋯ ∈ 𝓝 x

Tactic:
refine mem_of_superset ?_ (subset_biUnion_of_mem hyt)

Premises used: Set.subset_biUnion_of_mem, Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
x : X
hx : x ∈ s
y : (↑s : Type u)
hyt : y ∈ t
hy : x ∈ interior (U (↑y : X) ⋯)
⊢ U (↑y : X) ⋯ ∈ 𝓝 x

Tactic:
mem_interior_iff_mem_nhds.1 hy

Premises used: mem_interior_iff_mem_nhds, Iff.mp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
t : Finset (↑s : Type u)
hst : s ⊆ ⋃ i ∈ t, interior (U (↑i : X) ⋯)
x : X
hx : x ∈ s
y : (↑s : Type u)
hyt : y ∈ t
hy : x ∈ interior (U (↑y : X) ⋯)
⊢ U (↑y : X) ⋯ ∈ 𝓝 x

Tactic:
exact mem_interior_iff_mem_nhds.1 hy

Premises used: mem_interior_iff_mem_nhds, Iff.mp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
let :
  ∀ (t : Finset (↑s : Type u)) (ht : ⋃ x ∈ t, U (↑x : X) ∈ 𝓝ˢ s),
    ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
let ⟨t, ht⟩ := hs.elim_nhds_subcover_nhdsSet' (fun x _ => U x) hU
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset (↑s : Type u)
ht rwa rwa₁ rwa₂ rwa₃ : ⋃ y ∈ t, U (↑y : X) ∈ 𝓝ˢ s
⊢ ⋃ x ∈ Finset.image (Subtype.val (p := fun (x : X) ↦ x ∈ s)) t, U x ∈ 𝓝ˢ s

Tactic:
rwa [Finset.set_biUnion_finset_image]

Premises used: Finset.set_biUnion_finset_image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset (↑s : Type u)
ht : ⋃ x ∈ t, U (↑x : X) ∈ 𝓝ˢ s
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
exact ⟨t.image (↑), fun x hx =>
    let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
    hyx ▸ y.2,
    by rwa [Finset.set_biUnion_finset_image]⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
t : Finset (↑s : Type u)
ht : ⋃ x ∈ t, U (↑x : X) ∈ 𝓝ˢ s
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ ⋃ x ∈ t, U x ∈ 𝓝ˢ s

Tactic:
classical
  exact ⟨t.image (↑), fun x hx =>
    let ⟨y, _, hyx⟩ := Finset.mem_image.1 hx
    hyx ▸ y.2,
    by rwa [Finset.set_biUnion_finset_image]⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝 x
⊢ ∃ (t : Finset (↑s : Type u)), s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯

Tactic:
(hs.elim_nhds_subcover_nhdsSet' U hU).imp fun _ ↦ subset_of_mem_nhdsSet

Premises used: subset_of_mem_nhdsSet, Exists.imp, IsCompact.elim_nhds_subcover_nhdsSet'
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝 x
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
(hs.elim_nhds_subcover_nhdsSet hU).imp fun _ h ↦ h.imp_right subset_of_mem_nhdsSet

Premises used: Exists.imp, IsCompact.elim_nhds_subcover_nhdsSet
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
choose :
  ∀ (V : (x : X) → (hx : x ∈ s) → Set X) (V_nhds : ∀ (x : X) (hx : x ∈ s), V x hx ∈ 𝓝 x)
    (hV : ∀ (x : X) (hx : x ∈ s), V x hx ∩ s ⊆ U x hx), ∃ (t : Finset (↑s : Type u)), s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯
⊢ ∃ (t : Finset (↑s : Type u)), s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯

Tactic:
choose V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)

Premises used: Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
V : (x : X) → (hx : x ∈ s) → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x hx ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x hx ∩ s ⊆ U x hx
⊢ ∃ (t : Finset (↑s : Type u)), s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯

Tactic:
(hs.elim_nhds_subcover' V V_nhds).imp fun t ht =>
    subset_trans ?_ (iUnion₂_mono fun x _ => hV x x.2)

Premises used: subset_trans, Exists.imp, Set.iUnion₂_mono, IsCompact.elim_nhds_subcover', Subtype.val, Subtype.property
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
V : (x : X) → (hx : x ∈ s) → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x hx ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x hx ∩ s ⊆ U x hx
refine : ∀ (t : Finset (↑s : Type u)) (ht : s ⊆ ⋃ x ∈ t, V (↑x : X) ⋯), s ⊆ ⋃ i ∈ t, V (↑i : X) ⋯ ∩ s
⊢ ∃ (t : Finset (↑s : Type u)), s ⊆ ⋃ x ∈ t, U (↑x : X) ⋯

Tactic:
refine (hs.elim_nhds_subcover' V V_nhds).imp fun t ht =>
    subset_trans ?_ (iUnion₂_mono fun x _ => hV x x.2)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : (x : X) → x ∈ s → Set X
hU : ∀ (x : X) (hx : x ∈ s), U x hx ∈ 𝓝[s] x
V : (x : X) → (hx : x ∈ s) → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x hx ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x hx ∩ s ⊆ U x hx
t : Finset (↑s : Type u)
ht : s ⊆ ⋃ x ∈ t, V (↑x : X) ⋯
⊢ s ⊆ ⋃ i ∈ t, V (↑i : X) ⋯ ∩ s

Tactic:
simpa [← iUnion_inter, ← iUnion_coe_set]

Premises used: Set.iUnion_coe_set, Set.iUnion_inter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
choose! :
  ∀ (V : (x : X) → Set X) (V_nhds : ∀ (x : X) (hx : x ∈ s), V x ∈ 𝓝 x) (hV : ∀ (x : X) (hx : x ∈ s), V x ∩ s ⊆ U x),
    ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
choose! V V_nhds hV using fun x hx => mem_nhdsWithin_iff_exists_mem_nhds_inter.1 (hU x hx)

Premises used: Iff.mp, mem_nhdsWithin_iff_exists_mem_nhds_inter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
U : X → Set X
hU : ∀ x ∈ s, U x ∈ 𝓝[s] x
V : (x : X) → Set X
V_nhds : ∀ (x : X) (hx : x ∈ s), V x ∈ 𝓝 x
hV : ∀ (x : X) (hx : x ∈ s), V x ∩ s ⊆ U x
⊢ ∃ (t : Finset X), (∀ x ∈ t, x ∈ s) ∧ s ⊆ ⋃ x ∈ t, U x

Tactic:
(hs.elim_nhds_subcover V V_nhds).imp fun t ⟨t_sub_s, ht⟩ =>
    ⟨t_sub_s, subset_trans ?_ (iUnion₂_mono fun x hx => hV x (t_sub_s x hx))⟩

Premises used: Exists.imp, IsCompact.elim_nhds_subcover