rw [← diff_inter_self_eq_diff, ← diff_inter_self_eq_diff (t := r)]
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ s \ t = s \ r ↔ t ∩ s = r ∩ s
α : Type u_1
ι : Type u_2
s t r : Set α
⊢ s \ (t ∩ s) = s \ (r ∩ s) ↔ t ∩ s = r ∩ s