no goals
α : Type u_1
β : Type ?u.5636
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s : Set α
⊢ NoetherianSpace ↑s ↔ ∀ (t : Set α), t ⊆ s → IsCompact t
simp only [noetherianSpace_iff_isCompact, embedding_subtype_val.isCompact_iff_isCompact_image,
  Subtype.forall_set_subtype]