Theorem: Partition.eqv_class_comm (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 α
x : α
⊢ {y | r x y} = {y | r y x}
Tactic:
simp_rw [symm_iff_of]
State after:
no goals