Theorem: Partition.discrete.rel_iff_eq_of_mem (Matroid/ForMathlib/SetPartition.lean)

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z : α
s : Set α
a b : α
ha : a ∈ s
⊢ (Partition.discrete s).Rel a b ↔ a = b
Tactic:
rw [discrete.rel_iff_eq, and_iff_left ha]
State after:
no goals