refactor(combinatorics/simple_graph): simplify proofs (#6115)

Co-authors: `lean-gptf`, Stanislas Polu

This was found by `formal-lean-wm-to-tt-m1-m2-v4-c4` when we evaluated it on theorems added to `mathlib` after we last extracted training data.

src/combinatorics/simple_graph/basic.lean

@@ -212,10 +212,10 @@ lemma common_neighbors_symm (v w : V) : G.common_neighbors v w = G.common_neighb
 by { rw [common_neighbors, set.inter_comm], refl }
 
 lemma not_mem_common_neighbors_left (v w : V) : v ∉ G.common_neighbors v w :=
-by simp [common_neighbors]
+λ h, ne_of_adj G h.1 rfl
 
 lemma not_mem_common_neighbors_right (v w : V) : w ∉ G.common_neighbors v w :=
-by simp [common_neighbors]
+λ h, ne_of_adj G h.2 rfl
 
 lemma common_neighbors_subset_neighbor_set (v w : V) : G.common_neighbors v w ⊆ G.neighbor_set v :=
 by simp [common_neighbors]