## Stream: general

### Topic: symmetry fails if simple graph is imported

#### Bhavik Mehta (Mar 08 2021 at 03:27):

Here's my example:

import combinatorics.simple_graph.basic

example : true ↔ true :=
begin
symmetry,
end


fails with the error

invalid apply tactic, failed to unify
true ↔ true
with


and doesn't fail without the import.
Presumably this is from the symm attribute on simple_graph.edge_symm - should this be removed?

#### Kyle Miller (Mar 08 2021 at 06:13):

Yes, that attribute should be removed. There are no uses of symmetry when it comes to simple_graph.adj, but if it were somehow useful a fix would be to have a lemma that's an implication rather than a bi-implication:

@[symm] lemma edge_symm' (u v : V) : G.adj u v → G.adj v u := λ x, G.sym x


#### Bhavik Mehta (Mar 17 2021 at 16:11):

Done both in #6736

Last updated: May 14 2021 at 12:18 UTC