awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
i : Set X
hs : i = univ
⊢ ¬IsCompact.{u} (X := X) univ

Tactic:
noncompact_univ X

Premises used: noncompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
i : Set X
hs : i = univ
⊢ ¬IsCompact.{u} (X := X) univ

Tactic:
exact noncompact_univ X

Premises used: noncompact_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
⊢ cocompact X = ⊥

Tactic:
Filter.hasBasis_cocompact.eq_bot_iff.mpr ⟨Set.univ, isCompact_univ, Set.compl_univ⟩

Premises used: Iff.mpr, Filter.HasBasis.eq_bot_iff, Set.univ, Set.compl_univ, isCompact_univ, And.intro, Exists.intro, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
inst_2 : NoncompactSpace X
⊢ (coclosedCompact X).NeBot

Tactic:
neBot_of_le Filter.cocompact_le_coclosedCompact

Premises used: Filter.neBot_of_le, Filter.cocompact_le_coclosedCompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
h : (cocompact X).NeBot
⊢ NoncompactSpace X

Tactic:
⟨fun h' => (Filter.nonempty_of_mem h'.compl_mem_cocompact).ne_empty compl_univ⟩

Premises used: Set.Nonempty.ne_empty, IsCompact.compl_mem_cocompact, Filter.nonempty_of_mem, Set.compl_univ, NoncompactSpace.mk
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
⊢ (cocompact X).NeBot ↔ NoncompactSpace X

Tactic:
⟨noncompactSpace_of_neBot, fun _ => inferInstance⟩

Premises used: inferInstance, Iff.intro, noncompactSpace_of_neBot
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
⊢ ¬CompactSpace X ↔ NoncompactSpace X

Tactic:
⟨fun h₁ => ⟨fun h₂ => h₁ ⟨h₂⟩⟩, fun ⟨h₁⟩ ⟨h₂⟩ => h₁ h₂⟩

Premises used: False, _private.0.not_compactSpace_iff.match_2, CompactSpace.mk, Iff.intro, NoncompactSpace.mk, _private.0.not_compactSpace_iff.match_1
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
ι : Type u_1
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s t : Set X
f : X → Y
⊢ (cocompact ℤ).NeBot

Tactic:
simp only [Filter.cocompact_eq_cofinite, Filter.cofinite_neBot]

Premises used: Filter.cofinite_neBot, Filter.cocompact_eq_cofinite
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : DiscreteTopology X
⊢ Finite X

Tactic:
Finite.of_finite_univ <| isCompact_univ.finite_of_discrete

Premises used: isCompact_univ, IsCompact.finite_of_discrete, Finite.of_finite_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
x : X
hx : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
rwa : x ∈ K ∧ ClusterPt x (𝓟 {x}ᶜ ⊓ (cofinite ⊓ 𝓟 s))
rwa₁ : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s ⊓ 𝓟 {x}ᶜ)
rwa₂ : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 {x}ᶜ ⊓ 𝓟 s)
rwa₃ rwa₄ rwa₅ rwa₆ : x ∈ K ∧ ClusterPt x (cofinite ⊓ 𝓟 s)
⊢ x ∈ K ∧ AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
rwa [accPt_iff_clusterPt, inf_comm, inf_right_comm,
      (finite_singleton _).cofinite_inf_principal_compl]

Premises used: inf_comm, inf_right_comm, Set.finite_singleton, accPt_iff_clusterPt, Set.Finite.cofinite_inf_principal_compl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s K : Set X
hs : s.Infinite
hK : IsCompact K
hsub : s ⊆ K
⊢ ∃ x ∈ K, AccPt x (𝓟 s)

Tactic:
let ⟨x, hxK, hx⟩ := hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact hK hsub
  ⟨x, hxK, hx.mono inf_le_right⟩

Premises used: AccPt.mono, Membership.mem, Exists, inf_le_right, Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact, _private.0.Set.Infinite.exists_accPt_of_subset_isCompact.match_1, And, And.intro, Exists.intro, Filter.principal, AccPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : CompactSpace X
hs : s.Infinite
⊢ ∃ (x : X), AccPt x (cofinite ⊓ 𝓟 s)

Tactic:
simpa only [mem_univ, true_and]
    using hs.exists_accPt_cofinite_inf_principal_of_subset_isCompact isCompact_univ s.subset_univ

Premises used: Set.subset_univ, Set.Infinite.exists_accPt_cofinite_inf_principal_of_subset_isCompact, isCompact_univ, Set.mem_univ, true_and
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
inst_1 : CompactSpace X
hs : s.Infinite
⊢ ∃ (x : X), AccPt x (𝓟 s)

Tactic:
hs.exists_accPt_cofinite_inf_principal.imp fun _x hx ↦ hx.mono inf_le_right

Premises used: Set.Infinite.exists_accPt_cofinite_inf_principal, Exists.imp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : Infinite X
⊢ ∃ (z : X), (𝓝[≠] z).NeBot

Tactic:
simpa [AccPt] using (@infinite_univ X _).exists_accPt_principal

Premises used: Set.Infinite.exists_accPt_principal, Set.infinite_univ, AccPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ (t : Finset X), Eq.{u + 1} (α := Set X) (⋃ x ∈ t, interior (U x)) univ

Tactic:
let ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover (fun x => interior (U x))
    (fun _ => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
  ⟨t, univ_subset_iff.1 ht⟩

Premises used: Iff.mpr, Set.univ_subset_iff, mem_interior_iff_mem_nhds, isOpen_interior, Set.univ, Set.mem_iUnion, Exists, _private.0.finite_cover_nhds_interior.match_1, IsCompact.elim_finite_subcover, isCompact_univ, interior, Exists.intro, Iff.mp, Eq, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
U : X → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
⊢ ∃ (t : Finset X), Eq.{u + 1} (α := Set X) (⋃ x ∈ t, U x) univ

Tactic:
let ⟨t, ht⟩ := finite_cover_nhds_interior hU
  ⟨t, univ_subset_iff.1 <| ht.symm.subset.trans <| iUnion₂_mono fun _ _ => interior_subset⟩

Premises used: Set.univ_subset_iff, interior_subset, Set.univ, Exists, HasSubset.Subset.trans, Eq.subset, Set.iUnion₂_mono, finite_cover_nhds_interior, Exists.intro, Iff.mp, Eq.symm, Eq, Set.iUnion, _private.0.finite_cover_nhds.match_1
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
rw : ∀ (i' : Set X), IsCompact i' → ∃ (i : Set Y), IsCompact i ∧ f ⁻¹' iᶜ ⊆ i'ᶜ
⊢ comap f (cocompact Y) ≤ cocompact X

Tactic:
rw [(Filter.hasBasis_cocompact.comap f).le_basis_iff Filter.hasBasis_cocompact]

Premises used: Filter.HasBasis.le_basis_iff, Filter.HasBasis.comap, Filter.hasBasis_cocompact
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set X
ht : IsCompact t
⊢ ∃ (i : Set Y), IsCompact i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Tactic:
⟨f '' t, ht.image hf, ?_⟩

Premises used: And.intro, Exists.intro, Set.image, IsCompact.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set X
ht : IsCompact t
refine : f ⁻¹' (f '' t)ᶜ ⊆ tᶜ
⊢ ∃ (i : Set Y), IsCompact i ∧ f ⁻¹' iᶜ ⊆ tᶜ

Tactic:
refine ⟨f '' t, ht.image hf, ?_⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : Continuous[inst, inst_1] f
t : Set X
ht : IsCompact t
⊢ f ⁻¹' (f '' t)ᶜ ⊆ tᶜ

Tactic:
simpa using t.subset_preimage_image f

Premises used: Set.subset_preimage_image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst, inst_1] g
hf : Disjoint f (cocompact X)
rw : f ⊓ comap g (cocompact Y) ≤ ⊥
⊢ Disjoint (map g f) (cocompact Y)

Tactic:
rw [← Filter.disjoint_comap_iff_map, disjoint_iff_inf_le]

Premises used: Filter.disjoint_comap_iff_map, disjoint_iff_inf_le
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst, inst_1] g
hf : Disjoint f (cocompact X)
⊢ f ⊓ comap g (cocompact Y) ≤ f ⊓ cocompact X

Tactic:
inf_le_inf_left f (Filter.comap_cocompact_le hg)

Premises used: Set.Mem, Filter.comap_cocompact_le, inf_le_inf_left
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst, inst_1] g
hf : Disjoint f (cocompact X)
⊢ f ⊓ cocompact X = ⊥

Tactic:
disjoint_iff.mp hf

Premises used: disjoint_iff, Iff.mp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
g : X → Y
f : Filter X
hg : Continuous[inst, inst_1] g
hf : Disjoint f (cocompact X)
⊢ f ⊓ comap g (cocompact Y) ≤ ⊥

Tactic:
calc
    f ⊓ (comap g (cocompact Y))
    _ ≤ f ⊓ Filter.cocompact X := inf_le_inf_left f (Filter.comap_cocompact_le hg)
    _ = ⊥ := disjoint_iff.mp hf

Premises used: Filter.comap_cocompact_le, disjoint_iff, inf_le_inf_left, Filter.cocompact, Iff.mp, Filter.comap
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
rw : IsCompact (f '' univ)
⊢ IsCompact (range f)

Tactic:
rw [← image_univ]

Premises used: Set.image_univ
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsCompact (f '' univ)

Tactic:
isCompact_univ.image hf

Premises used: isCompact_univ, IsCompact.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : CompactSpace X
f : X → Y
hf : Continuous[inst, inst_1] f
⊢ IsCompact (f '' univ)

Tactic:
exact isCompact_univ.image hf

Premises used: isCompact_univ, IsCompact.image
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactSpace X
⊢ IsCompact (diagonal X)

Tactic:
@range_diag X ▸ isCompact_range (continuous_id.prodMk continuous_id)

Premises used: Eq.rec, isCompact_range, continuous_id, Set.range_diag, Continuous.prodMk
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
inst_1 : CompactSpace X
inst_2 : Nonempty ι
V : ι → Set X
hV : Directed (fun (x1 x2 : Set X) ↦ x1 ⊇ x2) V
hV_closed : ∀ (i : ι), IsClosed[inst] (V i)
U : Set X
hU : ∀ (x : X), Membership.mem (γ := Set X) (⋂ (i : ι), V i) x → U ∈ 𝓝 x
⊢ ∃ (i : ι), V i ⊆ U

Tactic:
exists_subset_nhds_of_isCompact' hV (fun i => (hV_closed i).isCompact) hV_closed hU

Premises used: IsClosed.isCompact, exists_subset_nhds_of_isCompact'
-- 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
hf : IsInducing f
⊢ IsCompact s ↔ IsCompact (f '' s)

Tactic:
⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot F_le => ?_⟩

Premises used: Iff.intro, Topology.IsInducing.continuous, IsCompact.image
-- 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
hf : IsInducing f
refine : ∀ (hs : IsCompact (f '' s)) (F : Filter X) (F_ne_bot : F.NeBot) (F_le : F ≤ 𝓟 s), ∃ x ∈ s, ClusterPt x F
⊢ IsCompact s ↔ IsCompact (f '' s)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot F_le => ?_⟩
-- 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
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
obtain : ∀ (x : X) (x_in : x ∈ s) (hx : ClusterPt (f x) (map f F)), ∃ x ∈ s, ClusterPt x F
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
    hs ((map_mono F_le).trans_eq map_principal)

Premises used: Filter.map_mono, LE.le.trans_eq, Filter.map_principal, 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
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Premises used: And.intro, Exists.intro, Iff.mp, Topology.IsInducing.mapClusterPt_iff
-- 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
hf : IsInducing f
hs : IsCompact (f '' s)
F : Filter X
F_ne_bot : F.NeBot
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩
-- 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
hf : IsEmbedding f
⊢ IsCompact s ↔ IsCompact (f '' s)

Tactic:
hf.isInducing.isCompact_iff

Premises used: Topology.IsEmbedding.isInducing, Topology.IsInducing.isCompact_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst_1] (range f)
K : Set Y
hK : IsCompact K
⊢ IsCompact (K ∩ range f)

Tactic:
replace hK := hK.inter_right hf'
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
hf' : IsClosed[inst_1] (range f)
K : Set Y
hK : IsCompact (K ∩ range f)
rwa : IsCompact (f '' f ⁻¹' K)
rwa₁ rwa₂ rwa₃ rwa₄ : IsCompact (K ∩ range f)
⊢ IsCompact (f ⁻¹' K)

Tactic:
rwa [hf.isCompact_iff, image_preimage_eq_inter_range]

Premises used: Set.image_preimage_eq_inter_range, Topology.IsInducing.isCompact_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
K : Set Y
Kf : K ⊆ range f
rw : IsCompact (f '' f ⁻¹' K) ↔ IsCompact K
rw₁ rw₂ : IsCompact K ↔ IsCompact K
⊢ IsCompact (f ⁻¹' K) ↔ IsCompact K

Tactic:
rw [hf.isCompact_iff, image_preimage_eq_of_subset Kf]

Premises used: Set.image_preimage_eq_of_subset, Topology.IsInducing.isCompact_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsInducing f
K : Set Y
hK : IsCompact K
Kf : K ⊆ range f
⊢ IsCompact (f ⁻¹' K)

Tactic:
(hf.isCompact_preimage_iff Kf).2 hK

Premises used: Iff.mpr, Topology.IsInducing.isCompact_preimage_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
K : Set Y
hK : IsCompact K
⊢ IsCompact (f ⁻¹' K)

Tactic:
hf.isInducing.isCompact_preimage (hf.isClosed_range) hK

Premises used: Topology.IsClosedEmbedding.isInducing, Topology.IsInducing.isCompact_preimage, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ Tendsto f (cocompact X) (cocompact Y)

Tactic:
Filter.hasBasis_cocompact.tendsto_right_iff.mpr fun _K hK =>
    (hf.isCompact_preimage hK).compl_mem_cocompact

Premises used: Iff.mpr, IsCompact.compl_mem_cocompact, Topology.IsClosedEmbedding.isCompact_preimage, Filter.hasBasis_cocompact, Filter.HasBasis.tendsto_right_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
p : X → Prop
s : Set { x : X // p x }
⊢ IsCompact s ↔ IsCompact (val (p := fun (x : X) ↦ p x) '' s)

Tactic:
IsEmbedding.subtypeVal.isCompact_iff

Premises used: Topology.IsEmbedding.isCompact_iff, Topology.IsEmbedding.subtypeVal
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
rw :
  IsCompact s ↔ IsCompact.{u} (X := X) (image (α := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)) univ)
rw₁ : IsCompact s ↔ IsCompact.{u} (X := X) (range (ι := { x : X // x ∈ s }) (Subtype.val (p := fun (x : X) ↦ x ∈ s)))
rw₂ rw₃ : IsCompact s ↔ IsCompact s
⊢ IsCompact s ↔ IsCompact.{u} (X := (↑s : Type u)) univ

Tactic:
rw [Subtype.isCompact_iff, image_univ, Subtype.range_coe]

Premises used: Set.image_univ, Subtype.isCompact_iff, Subtype.range_coe
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
this :
  Eq.{u_2 + 1} (α := Set (↑s : Type u_2))
    (univ ∩ ⋂ (i : (↑I : Type u_3)), (fun (i : (↑I : Type u_3)) ↦ (s ↓∩ t (↑i : ι) : Set (↑s : Type u_2))) i) ∅
⊢ ∃ (u : Finset (↑I : Type u_3)), s ∩ ⋂ i ∈ u, t (↑i : ι) = ∅

Tactic:
simpa [eq_empty_iff_forall_notMem] using
      (isCompact_iff_isCompact_univ.mp ks).elim_finite_subfamily_closed
      (fun i : I ↦ s ↓∩ t i) (fun i ↦ htc i.val i.prop) this

Premises used: isCompact_iff_isCompact_univ, Set.preimage, Set.eq_empty_iff_forall_notMem, Subtype.prop, Iff.mp, Subtype.val, IsCompact.elim_finite_subfamily_closed
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
suffices :
  Eq.{u_2 + 1} (α := Set (↑s : Type u_2))
    (univ ∩ ⋂ (i : (↑I : Type u_3)), (fun (i : (↑I : Type u_3)) ↦ (s ↓∩ t (↑i : ι) : Set (↑s : Type u_2))) i) ∅
⊢ ∃ (u : Finset (↑I : Type u_3)), s ∩ ⋂ i ∈ u, t (↑i : ι) = ∅

Tactic:
suffices univ ∩ ⋂ i, (fun i : I ↦ s ↓∩ t i) i = ∅ by
    simpa [eq_empty_iff_forall_notMem] using
      (isCompact_iff_isCompact_univ.mp ks).elim_finite_subfamily_closed
      (fun i : I ↦ s ↓∩ t i) (fun i ↦ htc i.val i.prop) this
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u_2
inst : TopologicalSpace X
s : Set X
ks : IsCompact s
ι : Type u_3
t : ι → Set X
I : Set ι
htc : ∀ i ∈ I, IsClosed[instTopologicalSpaceSubtype] (s ↓∩ t i)
hst : s ∩ ⋂ i ∈ I, t i = ∅
⊢ Eq.{u_2 + 1} (α := Set (↑s : Type u_2))
    (univ ∩ ⋂ (i : (↑I : Type u_3)), (fun (i : (↑I : Type u_3)) ↦ (s ↓∩ t (↑i : ι) : Set (↑s : Type u_2))) i) ∅

Tactic:
simpa [Set.eq_empty_iff_forall_notMem, Subtype.forall] using hst

Premises used: Subtype.forall, Set.eq_empty_iff_forall_notMem
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
⊢ IsCompact s ↔ CompactSpace.{u} (↑s : Type u)

Tactic:
isCompact_iff_isCompact_univ.trans isCompact_univ_iff

Premises used: isCompact_iff_isCompact_univ, isCompact_univ_iff, Iff.trans
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
hs' : IsDiscrete s
⊢ s.Finite

Tactic:
finite_coe_iff.mp (@finite_of_compact_of_discrete _ _
    (isCompact_iff_compactSpace.mp hs) hs'.to_subtype)

Premises used: finite_of_compact_of_discrete, Set.finite_coe_iff, Iff.mp
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
hs' : s.Infinite
⊢ ∃ z ∈ s, (𝓝[≠] z ⊓ 𝓟 s).NeBot

Tactic:
hs'.exists_accPt_of_subset_isCompact hs Subset.rfl

Premises used: Set.Infinite.exists_accPt_of_subset_isCompact, Set.Subset.rfl, AccPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : NoncompactSpace X
f : X → Y
hf : IsClosedEmbedding f
⊢ NoncompactSpace Y

Tactic:
noncompactSpace_of_neBot hf.tendsto_cocompact.neBot

Premises used: Topology.IsClosedEmbedding.tendsto_cocompact, Filter.Tendsto.neBot, noncompactSpace_of_neBot
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
rw : IsCompact (range f)
⊢ IsCompact.{u} (X := X) univ

Tactic:
rw [hf.isInducing.isCompact_iff, image_univ]

Premises used: Topology.IsClosedEmbedding.isInducing, Set.image_univ, Topology.IsInducing.isCompact_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)

Tactic:
hf.isClosed_range.isCompact

Premises used: IsClosed.isCompact, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
h : CompactSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsCompact (range f)

Tactic:
exact hf.isClosed_range.isCompact

Premises used: IsClosed.isCompact, Topology.IsClosedEmbedding.isClosed_range
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : IsCompact s
ht : IsCompact t
rw :
  ∀ (hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x)
    (ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x) (f : Ultrafilter (X × Y)),
    s ×ˢ t ∈ f → ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
⊢ IsCompact (s ×ˢ t)

Tactic:
rw [isCompact_iff_ultrafilter_le_nhds'] at hs ht ⊢

Premises used: isCompact_iff_ultrafilter_le_nhds'
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
obtain :
  ∀ (x : X) (sx : x ∈ s) (hx : map Prod.fst (↑f : Filter (X × Y)) ≤ 𝓝 x), ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x

Tactic:
obtain ⟨x : X, sx : x ∈ s, hx : map Prod.fst f.1 ≤ 𝓝 x⟩ :=
    hs (f.map Prod.fst) (mem_map.2 <| mem_of_superset hfs fun x => And.left)

Premises used: Iff.mpr, Filter.map, Prod.fst, And.left, Ultrafilter.map, Filter.mem_map, Ultrafilter.toFilter, Filter.mem_of_superset
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
s : Set X
t : Set Y
hs : ∀ (f : Ultrafilter X), s ∈ f → ∃ x ∈ s, (↑f : Filter X) ≤ 𝓝 x
ht : ∀ (f : Ultrafilter Y), t ∈ f → ∃ x ∈ t, (↑f : Filter Y) ≤ 𝓝 x
f : Ultrafilter (X × Y)
hfs : s ×ˢ t ∈ f
x : X
sx : x ∈ s
hx : map Prod.fst (↑f : Filter (X × Y)) ≤ 𝓝 x
obtain :
  ∀ (y : Y) (ty : y ∈ t) (hy : map Prod.snd (↑f : Filter (X × Y)) ≤ 𝓝 y), ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x
⊢ ∃ x ∈ s ×ˢ t, (↑f : Filter (X × Y)) ≤ 𝓝 x

Tactic:
obtain ⟨y : Y, ty : y ∈ t, hy : map Prod.snd f.1 ≤ 𝓝 y⟩ :=
    ht (f.map Prod.snd) (mem_map.2 <| mem_of_superset hfs fun x => And.right)

Premises used: Iff.mpr, Filter.map, And.right, Ultrafilter.map, Prod.snd, Filter.mem_map, Ultrafilter.toFilter, Filter.mem_of_superset