mathlib

3e79ce40 - chore(combinatorics/simple_graph/basic): remove unnecessary lemma (#14468)

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.