Theorem: Set.subset_diff_singleton_iff (Matroid/ForMathlib/Set.lean)

State before:
α : Type u_1
ι : Type u_2
s t : Set α
x : α
⊢ s ⊆ t \ {x} ↔ s ⊆ t ∧ x ∉ s
Tactic:
rw [subset_diff, disjoint_singleton_right]
State after:
no goals