mathlib3

[Merged by Bors] - feat(combinatorics/simple_graph): More clique lemmas

#19203

Closed