simp ignores direction of equation lemmas

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs,
      or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

When working with equation lemmas, simp only [←my_add] behaves as if it were simp only [my_add]: the ← is ignored.

Steps to Reproduce

def my_add (a b : nat) := a + b

example (a b : nat) : my_add a b - (a + b) = 0 :=
begin
  success_if_fail { simp only },  -- ok, nothing to simplify
  exact nat.sub_self _,
end

example (a b : nat) : my_add a b - (a + b) = 0 :=
begin
  simp only [my_add],
  guard_target a + b - (a + b) = 0, -- ok
  exact nat.sub_self _,
end

example (a b : nat) : my_add a b - (a + b) = 0 :=
begin
  simp only [←my_add],
  guard_target my_add a b - my_add a b, -- fail, goal is as if the `←` isn't there
  exac nat.sub_self _,
end

Expected behavior: [What you expect to happen]

The above code should produce no diagostics

Actual behavior: [What actually happens]

The final guard_target fails, as the goal is a + b - (a + b) = 0. Despite being told not to, simp unfolded my_add.

Start by running the self-contained reproducer using simp only [←my_add] and inspect the guard_target result. Trace the simp handling of equation lemmas and direction markers; done means the reversed lemma preserves my_add a b in the final goal and the reproducer passes without diagnostics.