chore(combinatorics/simple_graph/basic): remove unnecessary lemma (#1…

…4468) 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 · May 31, 2022 · 3e79ce4 · 3e79ce4
1 parent 1eb7339
commit 3e79ce4
Showing 1 changed file with 0 additions and 3 deletions.
diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean
@@ -475,9 +475,6 @@ fintype.card_of_subtype G.edge_finset (mem_edge_finset _)
 @[simp] lemma mem_neighbor_set (v w : V) : w ∈ G.neighbor_set v ↔ G.adj v w :=
 iff.rfl
 
-@[simp] lemma mem_neighbor_set' (v w : V) : G.neighbor_set v w ↔ G.adj v w :=
-iff.rfl
-
 @[simp] lemma mem_incidence_set (v w : V) : ⟦(v, w)⟧ ∈ G.incidence_set v ↔ G.adj v w :=
 by simp [incidence_set]