awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst] (s ∩ K)
K : Type u
x : TopologicalSpace K
h : CompactSpace K
h_1 : T2Space K
f : K → X
hf : Continuous[x, inst] f
⊢ IsClosed[x] (f ⁻¹' (s ∩ range f))

Tactic:
(hs (isCompact_range hf)).preimage hf

Premises used: isCompact_range, IsClosed.preimage
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsClosed[inst] (s ∩ K)
K : Type u
x : TopologicalSpace K
h : CompactSpace K
h_1 : T2Space K
f : K → X
hf : Continuous[x, inst] f
⊢ IsClosed[x] (f ⁻¹' (s ∩ range f))

Tactic:
exact (hs (isCompact_range hf)).preimage hf

Premises used: isCompact_range, IsClosed.preimage
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
h :
  ∀ (s : Set X),
    (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s)) →
      IsOpen[inst] s
⊢ CompactlyGeneratedSpace X

Tactic:
uCompactlyGeneratedSpace_of_isOpen fun s h' ↦ h s fun K _ _ _ f hf ↦ h' (CompHaus.of K) ⟨f, hf⟩

Premises used: uCompactlyGeneratedSpace_of_isOpen, ContinuousMap.mk, CompHaus.of
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsOpen (f ⁻¹' s)
⊢ IsOpen[inst] s

Tactic:
UCompactlyGeneratedSpace.isOpen fun S ⟨f, hf⟩ ↦ hs S f hf

Premises used: UCompactlyGeneratedSpace.isOpen, TopCat.carrier, Set.preimage, IsOpen, CompHausLike.toTop, DFunLike.coe, _private.0.continuous_from_compactlyGeneratedSpace.match_1
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst] (s ∩ K)
⊢ IsOpen[inst] s

Tactic:
isOpen' fun K _ _ _ f hf ↦ ?_

Premises used: CompactlyGeneratedSpace.isOpen'
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst] (s ∩ K)
refine :
  ∀ (K : Type u) (x : TopologicalSpace K),
    CompactSpace K → T2Space K → ∀ (f : K → X) (hf : Continuous[_, inst] f), IsOpen (f ⁻¹' s)
⊢ IsOpen[inst] s

Tactic:
refine isOpen' fun K _ _ _ f hf ↦ ?_

Premises used: CompactlyGeneratedSpace.isOpen'
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst] (s ∩ K)
K : Type u
x : TopologicalSpace K
h : CompactSpace K
h_1 : T2Space K
f : K → X
hf : Continuous[x, inst] f
rw : IsOpen[x] (f ⁻¹' (s ∩ range f))
⊢ IsOpen[x] (f ⁻¹' s)

Tactic:
rw [← Set.preimage_inter_range]

Premises used: Set.preimage_inter_range
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst] (s ∩ K)
K : Type u
x : TopologicalSpace K
h : CompactSpace K
h_1 : T2Space K
f : K → X
hf : Continuous[x, inst] f
⊢ IsOpen[x] (f ⁻¹' (s ∩ range f))

Tactic:
(hs (isCompact_range hf)).preimage hf

Premises used: isCompact_range, IsOpen.preimage
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : CompactlyGeneratedSpace X
s : Set X
hs : ∀ ⦃K : Set X⦄, IsCompact K → IsOpen[inst] (s ∩ K)
K : Type u
x : TopologicalSpace K
h : CompactSpace K
h_1 : T2Space K
f : K → X
hf : Continuous[x, inst] f
⊢ IsOpen[x] (f ⁻¹' (s ∩ range f))

Tactic:
exact (hs (isCompact_range hf)).preimage hf

Premises used: isCompact_range, IsOpen.preimage
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
tX : TopologicalSpace X
Y : Type u
tY : TopologicalSpace Y
inst : CompactlyGeneratedSpace X
f : X → Y
hf : Continuous[tX, tY] f
ht : tY = coinduced f tX
⊢ CompactlyGeneratedSpace Y

Tactic:
uCompactlyGeneratedSpace_of_coinduced hf ht

Premises used: uCompactlyGeneratedSpace_of_coinduced
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type u
Y : Type v
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactlyGeneratedSpace.{v} (X i)
⊢ CompactlyGeneratedSpace ((i : ι) × X i)

Tactic:
compactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sigma_iff.2 fun i ↦
    CompactlyGeneratedSpace.isClosed' fun K _ _ _ f hf ↦ ?_

Premises used: Iff.mpr, CompactlyGeneratedSpace.isClosed', isClosed_sigma_iff, compactlyGeneratedSpace_of_isClosed
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type u
Y : Type v
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactlyGeneratedSpace.{v} (X i)
refine :
  ∀ (s : Set ((i : ι) × X i))
    (h :
      ∀ (K : Type (max u v)) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → (i : ι) × X i),
        Continuous[_, instTopologicalSpaceSigma] f → IsClosed (f ⁻¹' s))
    (i : ι) (K : Type v) (x : TopologicalSpace K),
    CompactSpace K →
      T2Space K →
        ∀ (f : K → X i) (hf : Continuous[_, inst_2 i] f), IsClosed (f ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)
⊢ CompactlyGeneratedSpace ((i : ι) × X i)

Tactic:
refine compactlyGeneratedSpace_of_isClosed fun s h ↦ isClosed_sigma_iff.2 fun i ↦
    CompactlyGeneratedSpace.isClosed' fun K _ _ _ f hf ↦ ?_

Premises used: Iff.mpr, CompactlyGeneratedSpace.isClosed', isClosed_sigma_iff, compactlyGeneratedSpace_of_isClosed
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type u
Y : Type v
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactlyGeneratedSpace.{v} (X i)
s : Set ((i : ι) × X i)
h :
  ∀ (K : Type (max u v)) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → (i : ι) × X i),
    Continuous[_, instTopologicalSpaceSigma] f → IsClosed (f ⁻¹' s)
i : ι
K : Type v
x : TopologicalSpace K
h_1 : CompactSpace K
h_2 : T2Space K
f : K → X i
hf : Continuous[x, inst_2 i] f
g : ULift.{u, v} K → (i : ι) × X i := Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ f ∘ ULift.down
⊢ Continuous[ULift.topologicalSpace, instTopologicalSpaceSigma] g

Tactic:
have hg : Continuous g := continuous_sigmaMk.comp <| hf.comp continuous_uliftDown
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type u
Y : Type v
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactlyGeneratedSpace.{v} (X i)
s : Set ((i : ι) × X i)
h :
  ∀ (K : Type (max u v)) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → (i : ι) × X i),
    Continuous[_, instTopologicalSpaceSigma] f → IsClosed (f ⁻¹' s)
i : ι
K : Type v
x : TopologicalSpace K
h_1 : CompactSpace K
h_2 : T2Space K
f : K → X i
hf : Continuous[x, inst_2 i] f
g : ULift.{u, v} K → (i : ι) × X i := Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ f ∘ ULift.down
hg : Continuous[ULift.topologicalSpace, instTopologicalSpaceSigma] g
⊢ IsClosed[x] (f ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)

Tactic:
(h _ g hg).preimage continuous_uliftUp

Premises used: Set.Mem, setOf, continuous_uliftUp, Set.preimage, IsClosed.preimage
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X_1 : Type u
Y : Type v
inst : TopologicalSpace X_1
inst_1 : TopologicalSpace Y
ι : Type u
X : ι → Type v
inst_2 : (i : ι) → TopologicalSpace (X i)
inst_3 : ∀ (i : ι), CompactlyGeneratedSpace.{v} (X i)
s : Set ((i : ι) × X i)
h :
  ∀ (K : Type (max u v)) [inst : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → (i : ι) × X i),
    Continuous[_, instTopologicalSpaceSigma] f → IsClosed (f ⁻¹' s)
i : ι
K : Type v
x : TopologicalSpace K
h_1 : CompactSpace K
h_2 : T2Space K
f : K → X i
hf : Continuous[x, inst_2 i] f
g : ULift.{u, v} K → (i : ι) × X i := Sigma.mk (β := fun (i : ι) ↦ X i) i ∘ f ∘ ULift.down
hg : Continuous[ULift.topologicalSpace, instTopologicalSpaceSigma] g
⊢ IsClosed[x] (f ⁻¹' Sigma.mk (β := fun (i : ι) ↦ X i) i ⁻¹' s)

Tactic:
exact (h _ g hg).preimage continuous_uliftUp

Premises used: continuous_uliftUp, IsClosed.preimage
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
⊢ CompactlyGeneratedSpace X

Tactic:
compactlyGeneratedSpace_of_isClosed fun s hs ↦ h s fun K hK ↦ ?_

Premises used: compactlyGeneratedSpace_of_isClosed
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
refine :
  ∀ (s : Set X)
    (hs :
      ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
        Continuous[_, inst] f → IsClosed (f ⁻¹' s))
    (K : Set X) (hK : IsCompact K), IsClosed[inst] (s ∩ K)
⊢ CompactlyGeneratedSpace X

Tactic:
refine compactlyGeneratedSpace_of_isClosed fun s hs ↦ h s fun K hK ↦ ?_

Premises used: compactlyGeneratedSpace_of_isClosed
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
rw :
  IsClosed[inst]
    (image (α := { x : X // x ∈ K }) (Subtype.val (p := fun (x : X) ↦ x ∈ K))
      (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s))
⊢ IsClosed[inst] (s ∩ K)

Tactic:
rw [Set.inter_comm, ← Subtype.image_preimage_coe]

Premises used: Subtype.image_preimage_coe, Set.inter_comm
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
a : IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)
⊢ IsClosed[inst]
    (image (α := { x : X // x ∈ K }) (Subtype.val (p := fun (x : X) ↦ x ∈ K))
      (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s))

Tactic:
apply hK.isClosed.isClosedMap_subtype_val

Premises used: IsClosed.isClosedMap_subtype_val, IsCompact.isClosed
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ CompactSpace.{u} (↑K : Type u)

Tactic:
have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace.{u} (↑K : Type u)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)

Tactic:
hs _ Subtype.val continuous_subtype_val

Premises used: continuous_subtype_val, Subtype.val
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace.{u} (↑K : Type u)
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)

Tactic:
exact hs _ Subtype.val continuous_subtype_val

Premises used: continuous_subtype_val, Subtype.val
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst] s
⊢ CompactlyGeneratedSpace X

Tactic:
compactlyGeneratedSpace_of_isOpen fun s hs ↦ h s fun K hK ↦ ?_

Premises used: compactlyGeneratedSpace_of_isOpen
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst] s
refine :
  ∀ (s : Set X)
    (hs :
      ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
        Continuous[_, inst] f → IsOpen (f ⁻¹' s))
    (K : Set X) (hK : IsCompact K), IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)
⊢ CompactlyGeneratedSpace X

Tactic:
refine compactlyGeneratedSpace_of_isOpen fun s hs ↦ h s fun K hK ↦ ?_

Premises used: compactlyGeneratedSpace_of_isOpen
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ CompactSpace.{u} (↑K : Type u)

Tactic:
have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace.{u} (↑K : Type u)
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)

Tactic:
hs _ Subtype.val continuous_subtype_val

Premises used: continuous_subtype_val, Subtype.val
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
inst : TopologicalSpace X
inst_1 : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)) → IsOpen[inst] s
s : Set X
hs :
  ∀ (K : Type u) [inst_2 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
    Continuous[_, inst] f → IsOpen (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace.{u} (↑K : Type u)
⊢ IsOpen[instTopologicalSpaceSubtype] (K ↓∩ s)

Tactic:
exact hs _ Subtype.val continuous_subtype_val

Premises used: continuous_subtype_val, Subtype.val
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
⊢ CompactlyGeneratedSpace X

Tactic:
compactlyGeneratedSpace_of_isClosed_of_t2 fun s h ↦ ?_

Premises used: compactlyGeneratedSpace_of_isClosed_of_t2
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
refine : ∀ (s : Set X) (h : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)), IsClosed[inst] s
⊢ CompactlyGeneratedSpace X

Tactic:
refine compactlyGeneratedSpace_of_isClosed_of_t2 fun s h ↦ ?_

Premises used: compactlyGeneratedSpace_of_isClosed_of_t2
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
rw : ∀ (x : X) (F : Filter X), F.NeBot → F ≤ 𝓟 s → F ≤ 𝓝 x → x ∈ s
⊢ IsClosed[inst] s

Tactic:
rw [isClosed_iff_forall_filter]

Premises used: isClosed_iff_forall_filter
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
x : X
ℱ : Filter X
hℱ₁ : ℱ.NeBot
hℱ₂ : ℱ ≤ 𝓟 s
hℱ₃ : ℱ ≤ 𝓝 x
rcases : ∀ (K : Set X) (hK : IsCompact K) (K_mem : K ∈ 𝓝 x), x ∈ s
⊢ x ∈ s

Tactic:
rcases exists_compact_mem_nhds x with ⟨K, hK, K_mem⟩

Premises used: WeaklyLocallyCompactSpace.exists_compact_mem_nhds
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
x : X
ℱ : Filter X
hℱ₁ : ℱ.NeBot
hℱ₂ : ℱ ≤ 𝓟 s
hℱ₃ : ℱ ≤ 𝓝 x
K : Set X
hK : IsCompact K
K_mem : K ∈ 𝓝 x
⊢ x ∈ s

Tactic:
Set.mem_of_mem_inter_left <| isClosed_iff_forall_filter.1 (h _ hK) x ℱ hℱ₁
    (Filter.inf_principal ▸ le_inf hℱ₂ (le_trans hℱ₃ <| Filter.le_principal_iff.2 K_mem)) hℱ₃

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.inf_principal, Set.mem_of_mem_inter_left, Eq.rec, le_inf, Iff.mp, isClosed_iff_forall_filter, le_trans
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : WeaklyLocallyCompactSpace X
s : Set X
h : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
x : X
ℱ : Filter X
hℱ₁ : ℱ.NeBot
hℱ₂ : ℱ ≤ 𝓟 s
hℱ₃ : ℱ ≤ 𝓝 x
K : Set X
hK : IsCompact K
K_mem : K ∈ 𝓝 x
⊢ x ∈ s

Tactic:
exact Set.mem_of_mem_inter_left <| isClosed_iff_forall_filter.1 (h _ hK) x ℱ hℱ₁
    (Filter.inf_principal ▸ le_inf hℱ₂ (le_trans hℱ₃ <| Filter.le_principal_iff.2 K_mem)) hℱ₃

Premises used: Iff.mpr, Filter.le_principal_iff, Filter.inf_principal, Set.mem_of_mem_inter_left, Eq.rec, le_inf, Iff.mp, isClosed_iff_forall_filter, le_trans
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyGeneratedSpace X
⊢ CompactlyCoherentSpace X

Tactic:
CompactlyCoherentSpace.of_isOpen_forall_compactSpace fun _ h ↦ CompactlyGeneratedSpace.isOpen'
    fun K _ _ _ f hf ↦ h K f hf

Premises used: CompactlyCoherentSpace.of_isOpen_forall_compactSpace, CompactlyGeneratedSpace.isOpen'
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyCoherentSpace X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)) → IsClosed[inst] s
⊢ CompactlyGeneratedSpace X

Tactic:
apply compactlyGeneratedSpace_of_isClosed_of_t2

Premises used: compactlyGeneratedSpace_of_isClosed_of_t2
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
h : ∀ (K : Set X), IsCompact K → IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)
⊢ IsClosed[inst] s

Tactic:
rw [CompactlyCoherentSpace.isClosed_iff]

Premises used: CompactlyCoherentSpace.isClosed_iff
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
K : Set X
hK : IsCompact K
h : IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' (s ∩ K))
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' s)

Tactic:
rw [← Subtype.preimage_coe_inter_self]

Premises used: Subtype.preimage_coe_inter_self
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' (s ∩ K))

Tactic:
(hs K hK).preimage_val

Premises used: IsClosed.preimage_val
-- Module: Mathlib.Topology.Compactness.CompactlyGeneratedSpace
Goal:
X : Type u
Y : Type v
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
inst_2 : T2Space X
inst_3 : CompactlyCoherentSpace X
s : Set X
hs : ∀ (K : Set X), IsCompact K → IsClosed[inst] (s ∩ K)
K : Set X
hK : IsCompact K
⊢ IsClosed[instTopologicalSpaceSubtype] (Subtype.val (p := fun (x : X) ↦ x ∈ K) ⁻¹' (s ∩ K))

Tactic:
exact (hs K hK).preimage_val

Premises used: IsClosed.preimage_val
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
⊢ IsCountablyCompact.{u_2} (E := E) ∅

Tactic:
fun _f _ _ hle => absurd (empty_mem_iff_bot.mp (le_principal_iff.mp hle)) NeBot.ne'

Premises used: Filter.le_principal_iff, IsCountablyCompact, absurd, Filter.NeBot.ne', Filter.empty_mem_iff_bot, Iff.mp
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
x : E
⊢ IsCountablyCompact (E := E) {x}

Tactic:
fun _ _ _ hle ↦
  ⟨x, rfl, ClusterPt.of_le_nhds <| hle.trans (principal_singleton x ▸ pure_le_nhds x)⟩

Premises used: ClusterPt.of_le_nhds, pure_le_nhds, Eq.rec, IsCountablyCompact, Filter.principal_singleton, And.intro, Exists.intro, LE.le.trans, Eq.symm, rfl
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A B : Set E
hA : IsCountablyCompact A
hB : IsClosed[inst] B
hBA : B ⊆ A
⊢ IsCountablyCompact B

Tactic:
fun _f _ _ hle ↦
  let ⟨a, _, hac⟩ := hA (hle.trans (principal_mono.mpr hBA))
  ⟨a, isClosed_iff_clusterPt.mp hB a (hac.mono hle), hac⟩

Premises used: Iff.mpr, ClusterPt.mono, Filter.principal_mono, Membership.mem, Exists, IsCountablyCompact, ClusterPt, And, isClosed_iff_clusterPt, And.intro, Exists.intro, Iff.mp, LE.le.trans, _private.0.IsCountablyCompact.of_isClosed_subset.match_1
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
inst_1 : CountablyCompactSpace E
hA : IsClosed[inst] A
⊢ IsCountablyCompact A

Tactic:
CountablyCompactSpace.isCountablyCompact_univ.of_isClosed_subset hA (subset_univ _)

Premises used: Set.subset_univ, CountablyCompactSpace.isCountablyCompact_univ, IsCountablyCompact.of_isClosed_subset
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
h : f.NeBot
h_1 : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
obtain : ∀ (x : ℕ → E) (hx : Tendsto x atTop f), ∃ a ∈ A, ClusterPt a f
⊢ ∃ a ∈ A, ClusterPt a f

Tactic:
obtain ⟨x, hx⟩ := f.exists_seq_tendsto

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.Topology.Compactness.CountablyCompact
Goal:
E : Type u_2
inst : TopologicalSpace E
A : Set E
hA : ∀ (x : ℕ → E), (∀ᶠ (n : ℕ) in atTop, x n ∈ A) → ∃ a ∈ A, MapClusterPt a atTop x
f : Filter E
h : f.NeBot
h_1 : f.IsCountablyGenerated
hle : f ≤ 𝓟 A
x : ℕ → E
hx : Tendsto x atTop f
⊢ ∀ᶠ (n : ℕ) in atTop, x n ∈ A

Tactic:
simpa using hx.mono_right hle

Premises used: Filter.Tendsto.mono_right