-- Mathlib/Topology/Compactness/CompactlyGeneratedSpace.lean
theorem compactlyGeneratedSpace_of_isClosed_of_t2
    (h : ∀ s, (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s) :
    CompactlyGeneratedSpace X

Proof state:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed (Subtype.val ⁻¹' s)

Tactic:
have : CompactSpace ↑K := isCompact_iff_compactSpace.1 hK

Result:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace ↑K
⊢ IsClosed (Subtype.val ⁻¹' s)

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed (Subtype.val '' (Subtype.val ⁻¹' s))

Tactic:
apply hK.isClosed.isClosedMap_subtype_val

Result:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed (Subtype.val ⁻¹' s)

Proof state:
case a
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
this : CompactSpace ↑K
⊢ IsClosed (Subtype.val ⁻¹' s)

Tactic:
exact hs _ Subtype.val continuous_subtype_val

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
⊢ CompactlyGeneratedSpace X

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

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed (s ∩ K)

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed (s ∩ K)

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

Result:
X : Type u
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
h : ∀ (s : Set X), (∀ (K : Set X), IsCompact K → IsClosed (s ∩ K)) → IsClosed s
s : Set X
hs :
  ∀ (K : Type u) [inst : TopologicalSpace K] [inst_1 : CompactSpace K] [inst_2 : T2Space K] (f : K → X),
    Continuous f → IsClosed (f ⁻¹' s)
K : Set X
hK : IsCompact K
⊢ IsClosed (Subtype.val '' (Subtype.val ⁻¹' s))