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.





leanprover-community/mathlib,leanprover-community/mathlib