symmetry fails if simple graph is imported

Stream: general

[Bhavik Mehta]

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
  ?m_2.adj ?m_3 ?m_4 ↔ ?m_2.adj ?m_4 ?m_3

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]

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]

Done both in #6736