simp only [mem_union, mem_diff]
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s \ t ∪ r ↔ x ∈ s ∪ r
case h
α : Type u_1
ι : Type u_2
s t r : Set α
h : t ⊆ r
x : α
⊢ x ∈ s ∧ x ∉ t ∨ x ∈ r ↔ x ∈ s ∨ x ∈ r