symmetric.iff

Stream: Is there code for X?

[Jalex Stark]

what should I use when I want to rw the symmetry of a symmetric relation?

lemma symmetric.iff {α : Type*} {r : α → α → Prop}
(h : symmetric r) (a b : α) : r a b ↔ r b a :=
by split; apply h

[Johan Commelin]

I would guess there is a lemma close to the definition of symmetric.

[Bryan Gin-ge Chen]

symmetric is defined in core: docs#symmetric and there don't seem to be any lemmas about it there (nor in logic.basic or logic.relation).