rw [sdiff_eq_left, disjoint_iff_inter_eq_empty, inter_eq_self_of_subset_right hst] at h_eq
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : t \ s = t
⊢ False
α : Type u_1
ι : Type u_2
s t : Set α
hst : s ⊆ t
hs : s.Nonempty
h_eq : s = ∅
⊢ False