Theorem: toSubset_compact (Sard/ToSubset.lean)

State before:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s t : Set X
hsw : s ⊆ t
hs : IsCompact s
⊢ IsCompact (s.toSubset t)
Tactic:
sorry
State after:
no goals