Commit 2022-05-31 11:57 3e79ce40
View on Github →chore(combinatorics/simple_graph/basic): remove unnecessary lemma (#14468) This lemma was added in #11371 for the Lean version bump, since the more powerful congr lemmas revealed a bug in fintype instances that were finally corrected in #14136.