mathlib3

7413128c - feat(data/list/cycle): well-founded or transitive irreflexive relations don't have cycles (#18512)

feat(data/list/cycle): well-founded or transitive irreflexive relations don't have cycles (#18512) Since `simp` can prove statements such as `cycle r [a, b, c] ↔ r a b ∧ r b c ∧ r c a`, this gives us a nice generalization of asymmetry. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>