awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩

Premises used: le_antisymm, Set.toFinite, SetLike.coe, And.intro, Exists.intro, Finset.image
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
refine_1 : U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
refine_2 : ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i ≤ U
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
refine ⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
⊢ U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i

Tactic:
Set.Subset.trans ht ?_

Premises used: Set.Subset.trans
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
refine_1 : Subset.{u_1} (α := Set X) (⋃ i ∈ t, (b ∘ f') i) (⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i)
⊢ U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i

Tactic:
refine Set.Subset.trans ht ?_

Premises used: Set.Subset.trans
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
refine_1 : ∀ (i : Y) (i_1 : i ∈ t), (b ∘ f') i ⊆ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
⊢ Subset.{u_1} (α := Set X) (⋃ i ∈ t, (b ∘ f') i) (⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i)

Tactic:
simp only [Set.iUnion_subset_iff]

Premises used: Set.iUnion_subset_iff
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
i : Y
hi : i ∈ t
⊢ (b ∘ f') i ⊆ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i

Tactic:
simpa using subset_iUnion₂ (s := fun i _ => b (f' i)) i hi

Premises used: Set.subset_iUnion₂
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
refine_2 : ∀ (i : ι) (j : i ∈ (↑(Finset.image f' t) : Set ι)), b i ⊆ U
⊢ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i ≤ U

Tactic:
apply Set.iUnion₂_subset

Premises used: Set.iUnion₂_subset
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
i : ι
hi : i ∈ (↑(Finset.image f' t) : Set ι)
refine_2 : ∀ (j : Y) (hi : f' j ∈ (↑(Finset.image f' t) : Set ι)), b (f' j) ⊆ U
⊢ b i ⊆ U

Tactic:
obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi

Premises used: Finset.mem_image, Iff.mp, rfl
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
j : Y
hi : f' j ∈ (↑(Finset.image f' t) : Set ι)
refine_2 : b (f' j) ⊆ ⋃ (i : Y), (b ∘ f') i
⊢ b (f' j) ⊆ U

Tactic:
rw [e]
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
j : Y
hi : f' j ∈ (↑(Finset.image f' t) : Set ι)
⊢ b (f' j) ⊆ ⋃ (i : Y), (b ∘ f') i

Tactic:
Set.subset_iUnion (b ∘ f') j

Premises used: Function.comp, Set.subset_iUnion
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
j : Y
hi : f' j ∈ (↑(Finset.image f' t) : Set ι)
⊢ b (f' j) ⊆ ⋃ (i : Y), (b ∘ f') i

Tactic:
exact Set.subset_iUnion (b ∘ f') j

Premises used: Function.comp, Set.subset_iUnion
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
U : Set X
hUc : IsCompact U
hUo : IsOpen U
Y : Type u_1
f' : (i : Y) → ι
e : U = ⋃ (i : Y), (b ∘ f') i
hf' : ∀ (i : Y), b (f' i) = (b ∘ f') i
t : Finset Y
ht : U ⊆ ⋃ i ∈ t, (b ∘ f') i
refine_1 : U ≤ ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i
refine_2 refine_2₁ : ⋃ i ∈ (↑(Finset.image f' t) : Set ι), b i ≤ U
⊢ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
classical
  refine ⟨t.image f', Set.toFinite _, le_antisymm ?_ ?_⟩
  · refine Set.Subset.trans ht ?_
    simp only [Set.iUnion_subset_iff]
    intro i hi
    simpa using subset_iUnion₂ (s := fun i _ => b (f' i)) i hi
  · apply Set.iUnion₂_subset
    rintro i hi
    obtain ⟨j, -, rfl⟩ := Finset.mem_image.mp hi
    rw [e]
    exact Set.subset_iUnion (b ∘ f') j

Premises used: Set.iUnion₂_subset, Set.iUnion_subset_iff, Set.Subset.trans, rfl
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)

Tactic:
simp
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
⊢ b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)

Tactic:
have hb' : b = range (fun i ↦ i : b → Set X) := by simp
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis b
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
rw :
  ∀ (hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))) (U : Set X)
    (hUc : IsCompact U) (hUo : IsOpen U) (hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)),
    ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
⊢ ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))

Tactic:
rw [hb'] at hb
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
choose :
  ∀ (s : Set (↑b : Type u_1)) (hs : s.Finite) (hU : U = ⋃ i ∈ s, (↑i : Set X)),
    ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))
⊢ ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))

Tactic:
choose s hs hU using eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U hUc hUo

Premises used: eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
s : Set (↑b : Type u_1)
hs : s.Finite
hU : U = ⋃ i ∈ s, (↑i : Set X)
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
have : Finite s := hs
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
s : Set (↑b : Type u_1)
hs : s.Finite
hU : U = ⋃ i ∈ s, (↑i : Set X)
this : Finite.{u_1 + 1} (↑s : Type u_1)
x : Fintype (↑s : Type u_1) := Fintype.ofFinite (↑s : Type u_1)
h : U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s.toFinset : Set (↑b : Type u_1)))
⊢ ∃ (s : Finset (↑b : Type u_1)), U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s : Set (↑b : Type u_1)))

Tactic:
use s.toFinset

Premises used: Set.toFinset
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
inst : TopologicalSpace X
b : Set (Set X)
hb : IsTopologicalBasis.{u_1} (α := X) (range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X))
U : Set X
hUc : IsCompact U
hUo : IsOpen U
hb' : b = range fun (i : (↑b : Type u_1)) ↦ (↑i : Set X)
s : Set (↑b : Type u_1)
hs : s.Finite
hU : U = ⋃ i ∈ s, (↑i : Set X)
this : Finite.{u_1 + 1} (↑s : Type u_1)
x : Fintype (↑s : Type u_1) := Fintype.ofFinite (↑s : Type u_1)
⊢ U = ⋃₀ (Subtype.val (p := fun (x : Set X) ↦ x ∈ b) '' (↑s.toFinset : Set (↑b : Type u_1)))

Tactic:
simp [hU]
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
mp : IsCompact U ∧ IsOpen U → ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i
mpr : (∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i) → IsCompact U ∧ IsOpen U
⊢ IsCompact U ∧ IsOpen U ↔ ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U → ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
fun ⟨h₁, h₂⟩ ↦ eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U h₁ h₂

Premises used: _private.0.isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis.match_1, eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open, Set.Finite, Exists, And, Eq, Set.iUnion
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
U : Set X
⊢ IsCompact U ∧ IsOpen U → ∃ (s : Set ι), s.Finite ∧ U = ⋃ i ∈ s, b i

Tactic:
exact fun ⟨h₁, h₂⟩ ↦ eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open _ hb U h₁ h₂
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
mpr : IsCompact.{u_1} (X := X) (⋃ i ∈ s, b i)
mpr₁ : IsOpen.{u_1} (X := X) (⋃ i ∈ s, b i)
⊢ IsCompact.{u_1} (X := X) (⋃ i ∈ s, b i) ∧ IsOpen.{u_1} (X := X) (⋃ i ∈ s, b i)

Tactic:
constructor
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact.{u_1} (X := X) (⋃ i ∈ s, b i)

Tactic:
hs.isCompact_biUnion fun i _ => hb' i

Premises used: Set.Finite.isCompact_biUnion
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsCompact.{u_1} (X := X) (⋃ i ∈ s, b i)

Tactic:
exact hs.isCompact_biUnion fun i _ => hb' i

Premises used: Set.Finite.isCompact_biUnion
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsOpen.{u_1} (X := X) (⋃ i ∈ s, b i)

Tactic:
isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

Premises used: Set.mem_range_self, TopologicalSpace.IsTopologicalBasis.isOpen, isOpen_biUnion
-- Module: Mathlib.Topology.Compactness.Bases
Goal:
X : Type u_1
ι : Type u_2
inst : TopologicalSpace X
b : ι → Set X
hb : IsTopologicalBasis (range b)
hb' : ∀ (i : ι), IsCompact (b i)
s : Set ι
hs : s.Finite
⊢ IsOpen.{u_1} (X := X) (⋃ i ∈ s, b i)

Tactic:
exact isOpen_biUnion fun i _ => hb.isOpen (Set.mem_range_self _)

Premises used: Set.mem_range_self, TopologicalSpace.IsTopologicalBasis.isOpen, isOpen_biUnion
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
inst_1 : f.NeBot
hf : f ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x f

Tactic:
hs hf
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
ι : Type u_2
hs : IsCompact s
f : Filter ι
inst_1 : f.NeBot
u : ι → X
hf : map u f ≤ 𝓟 s
⊢ ∃ x ∈ s, MapClusterPt x f u

Tactic:
hs hf

Premises used: MapClusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
l : Filter X
hs : IsCompact s
hl : ∃ᶠ (x : X) in l, x ∈ s
⊢ ∃ a ∈ s, ClusterPt a l

Tactic:
let ⟨a, has, ha⟩ := @hs _ (frequently_mem_iff_neBot.mp hl) inf_le_right
  ⟨a, has, ha.mono inf_le_left⟩

Premises used: ClusterPt.mono, Membership.mem, Exists, inf_le_right, _private.0.IsCompact.exists_clusterPt_of_frequently.match_1, ClusterPt, And, And.intro, Exists.intro, inf_le_left
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
ι : Type u_1
inst : TopologicalSpace X
s : Set X
l : Filter ι
f : ι → X
hs : IsCompact s
hf : ∃ᶠ (x : ι) in l, f x ∈ s
⊢ ∃ a ∈ s, MapClusterPt a l f

Tactic:
hs.exists_clusterPt_of_frequently hf

Premises used: MapClusterPt, IsCompact.exists_clusterPt_of_frequently
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, sᶜ ∈ 𝓝 x ⊓ f
contrapose! : ∀ (hf : sᶜ ∉ f), ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f
⊢ sᶜ ∈ f

Tactic:
contrapose! hf
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : sᶜ ∉ f
simp : ∀ (hf : (f ⊓ 𝓟 s).NeBot), ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot
⊢ ∃ x ∈ s, sᶜ ∉ 𝓝 x ⊓ f

Tactic:
simp only [notMem_iff_inf_principal_compl, compl_compl, inf_assoc] at hf ⊢

Premises used: compl_compl, Filter.notMem_iff_inf_principal_compl, inf_assoc
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Tactic:
@hs _ hf inf_le_right

Premises used: inf_le_right, ClusterPt
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : (f ⊓ 𝓟 s).NeBot
⊢ ∃ x ∈ s, (𝓝 x ⊓ (f ⊓ 𝓟 s)).NeBot

Tactic:
exact @hs _ hf inf_le_right

Premises used: inf_le_right
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
⊢ sᶜ ∈ f

Tactic:
hs.compl_mem_sets fun x hx => ?_

Premises used: IsCompact.compl_mem_sets
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
refine : ∀ (x : X) (hx : x ∈ s), sᶜ ∈ 𝓝 x ⊓ f
⊢ sᶜ ∈ f

Tactic:
refine hs.compl_mem_sets fun x hx => ?_

Premises used: IsCompact.compl_mem_sets
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
rcases : ∀ (t : Set X) (ht : t ∈ 𝓝[s] x) (hst : tᶜ ∈ f), sᶜ ∈ 𝓝 x ⊓ f
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
rcases hf x hx with ⟨t, ht, hst⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hst : tᶜ ∈ f
⊢ {x : X | x ∈ s → x ∈ t} ∈ 𝓝 x

Tactic:
replace ht := mem_inf_principal.1 ht
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x : X | x ∈ s → x ∈ t} ∈ 𝓝 x
apply : {x : X | x ∈ s → x ∈ t} ∩ tᶜ ⊆ sᶜ
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
apply mem_inf_of_inter ht hst

Premises used: Filter.mem_inf_of_inter
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs_1 : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x_1 : X
hx : x_1 ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x : X | x ∈ s → x ∈ t} ∈ 𝓝 x_1
x : X
h₁ : Membership.mem (γ := Set X) {x : X | x ∈ s → x ∈ t} x
h₂ : x ∈ tᶜ
hs : x ∈ s
⊢ False

Tactic:
h₂ (h₁ hs)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs_1 : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x_1 : X
hx : x_1 ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x : X | x ∈ s → x ∈ t} ∈ 𝓝 x_1
x : X
h₁ : Membership.mem (γ := Set X) {x : X | x ∈ s → x ∈ t} x
h₂ : x ∈ tᶜ
hs : x ∈ s
⊢ False

Tactic:
exact h₂ (h₁ hs)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
let : p s
⊢ p s

Tactic:
let f : Filter X := comk p he (fun _t ht _s hsub ↦ hmono hsub ht) (fun _s hs _t ht ↦ hunion hs ht)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f

Tactic:
simpa [f] using hnhds
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
⊢ sᶜ ∈ f

Tactic:
have : sᶜ ∈ f := hs.compl_mem_sets_of_nhdsWithin (by simpa [f] using hnhds)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s : Set X
hs : IsCompact s
p : Set X → Prop
he : p ∅
hmono : ∀ ⦃s t : Set X⦄, s ⊆ t → p t → p s
hunion : ∀ ⦃s t : Set X⦄, p s → p t → p (s ∪ t)
hnhds : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, p t
f : Filter X := comk p he ⋯ ⋯
this : sᶜ ∈ f
rwa rwa₁ rwa₂ rwa₃ : p sᶜᶜ
⊢ p s

Tactic:
rwa [← compl_compl s]

Premises used: compl_compl
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
⊢ ∃ x ∈ s, ClusterPt x f

Tactic:
hs (le_trans hstf (le_principal_iff.2 inter_subset_left))

Premises used: Iff.mpr, Filter.le_principal_iff, Set.inter_subset_left, le_trans
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
obtain : ∀ (x : X) (hsx : x ∈ s) (hx : ClusterPt x f), ∃ x ∈ s ∩ t, ClusterPt x f
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
obtain ⟨x, hsx, hx⟩ : ∃ x ∈ s, ClusterPt x f :=
    hs (le_trans hstf (le_principal_iff.2 inter_subset_left))

Premises used: Iff.mpr, Filter.le_principal_iff, Set.inter_subset_left, le_trans
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
⊢ x ∈ t

Tactic:
have : x ∈ t := ht.mem_of_nhdsWithin_neBot <|
    hx.mono <| le_trans hstf (le_principal_iff.2 inter_subset_right)
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
this : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
⟨x, ⟨hsx, this⟩, hx⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
f : Filter X
hnf : f.NeBot
hstf : f ≤ 𝓟 (s ∩ t)
x : X
hsx : x ∈ s
hx : ClusterPt x f
this : x ∈ t
⊢ ∃ x ∈ s ∩ t, ClusterPt x f

Tactic:
exact ⟨x, ⟨hsx, this⟩, hx⟩
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
ht : IsCompact t
hs : IsClosed[inst] s
⊢ IsCompact (s ∩ t)

Tactic:
inter_comm t s ▸ ht.inter_right hs

Premises used: Eq.rec, Set.inter_comm, IsCompact.inter_right
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsOpen[inst] t
⊢ IsCompact (s \ t)

Tactic:
hs.inter_right (isClosed_compl_iff.mpr ht)

Premises used: Iff.mpr, Set.Mem, Set.diff, setOf, IsCompact.inter_right, Not, isClosed_compl_iff
-- Module: Mathlib.Topology.Compactness.Compact
Goal:
X : Type u
inst : TopologicalSpace X
s t : Set X
hs : IsCompact s
ht : IsClosed[inst] t
h : t ⊆ s
⊢ IsCompact t

Tactic:
inter_eq_self_of_subset_right h ▸ hs.inter_right ht

Premises used: Eq.rec, Set.inter_eq_self_of_subset_right, IsCompact.inter_right
-- 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)
⊢ (comap f l ⊓ 𝓟 s).NeBot

Tactic:
have : NeBot (l.comap f ⊓ 𝓟 s) :=
    comap_inf_principal_neBot_of_image_mem lne (le_principal_iff.1 ls)
-- 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 ∈ s, ClusterPt x (comap f l ⊓ 𝓟 s)

Tactic:
@hs _ this inf_le_right

Premises used: inf_le_right
-- 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
obtain : ∀ (x : X) (hxs : x ∈ s) (hx : ClusterPt x (comap f l ⊓ 𝓟 s)), ∃ x ∈ f '' s, ClusterPt x l
⊢ ∃ x ∈ f '' s, ClusterPt x l

Tactic:
obtain ⟨x, hxs, hx⟩ : ∃ x ∈ s, ClusterPt x (l.comap f ⊓ 𝓟 s) := @hs _ this inf_le_right

Premises used: inf_le_right