no goals
α : Type u_1
β : Type u_2
γ : Type ?u.325947
δ : Type ?u.325950
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s t : Set α
x : α
ht : ContinuousWithinAt f t x
h : ContinuousWithinAt f (s \ t) x
⊢ s ⊆ s \ t ∪ t
simp only [diff_union_self, subset_union_left]