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

State before:
α : Type u_1
inst✝ : CompleteLattice α
s✝ x y z : α
s : Set α
a b : α
⊢ (Partition.discrete s).Rel a b ↔ a = b ∧ a ∈ s
Tactic:
simp only [Partition.discrete, ofRel', rel_congr, rel_ofRel_eq]
State after:
no goals