From 6e1143ab250c07a903a886b6bd4b1015272c7709 Mon Sep 17 00:00:00 2001 From: Bhavik Mehta Date: Wed, 17 Mar 2021 19:18:33 +0000 Subject: [PATCH] chore(combinatorics/simple_graph): remove bad simp attribute (#6736) As in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/symmetry.20fails.20if.20simple.20graph.20is.20imported. --- src/combinatorics/simple_graph/basic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/combinatorics/simple_graph/basic.lean b/src/combinatorics/simple_graph/basic.lean index 2b5d887313e15..9e79bb11fa73e 100644 --- a/src/combinatorics/simple_graph/basic.lean +++ b/src/combinatorics/simple_graph/basic.lean @@ -174,7 +174,9 @@ fintype.card_of_subtype G.edge_finset (mem_edge_finset _) @[simp] lemma irrefl {v : V} : ¬G.adj v v := G.loopless v -@[symm] lemma edge_symm (u v : V) : G.adj u v ↔ G.adj v u := ⟨λ x, G.sym x, λ x, G.sym x⟩ +lemma edge_symm (u v : V) : G.adj u v ↔ G.adj v u := ⟨λ x, G.sym x, λ x, G.sym x⟩ + +@[symm] lemma edge_symm' {u v : V} (h : G.adj u v) : G.adj v u := G.sym h @[simp] lemma mem_neighbor_set (v w : V) : w ∈ G.neighbor_set v ↔ G.adj v w := iff.rfl