Theorem: Partition.rel_self_iff_mem (Matroid/ForMathlib/SetPartition.lean)

State before:
α : Type u_1
inst✝² : CompleteLattice α
s✝¹ x y z : α
s✝ t : Set α
a b : α
P✝ : Partition s✝
r : α → α → Prop
inst✝¹ : IsSymm α r
inst✝ : IsTrans α r
s : Set α
P : Partition s
⊢ P.Rel x x ↔ x ∈ s
Tactic:
simp [← P.setOf_rel_self_eq]
State after:
no goals