Theorem: LocallyLipschitz.ToSubset.compatible_with_nhds (Sard/LocallyLipschitz.lean)

State before:
X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
inst✝ : MetricSpace Z
s t : Set X
x : ↑s
ht : t ∈ 𝓝 ↑x
⊢ t.toSubset s ∈ 𝓝 x
Tactic:
sorry
State after:
no goals