nth_rewrite can't rewrite inside of an implication

Stream: general

[Artem Vasilev]

The nth_rewrite tactic doesn't seem to find rewrite inside of an implication. Here is an example:

import tactic

example (n m k : ℕ) (h : m = k) : n ≤ m → n ≤ m :=
begin
  -- rw h, works, replaces both m's
  -- rw [h] {occs := occurrences.pos [1]}, works, replaces the first m
  -- nth_rewrite 0 h, fails, "not enough rewrites found"
  sorry,
end

Is this a bug? Should I create an issue on Github instead?

[Scott Morrison]

Interesting... want to try to fix it? :-) I wrote nth_rewrite, but I admit I'm not that keen on debugging it at the moment.

[Yaël Dillies]

I had the same problem with nth_rewrite_lhs/rhs