{"action":"opened","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/531","labels_url":"https://api.github.com/repos/leanprover/lean/issues/531/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/531/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/531/events","html_url":"https://github.com/leanprover/lean/issues/531","id":66263884,"number":531,"title":"rewrite fails after giving complete pattern","user":{"login":"fpvandoorn","id":7376012,"avatar_url":"https://avatars.githubusercontent.com/u/7376012?v=3","gravatar_id":"","url":"https://api.github.com/users/fpvandoorn","html_url":"https://github.com/fpvandoorn","followers_url":"https://api.github.com/users/fpvandoorn/followers","following_url":"https://api.github.com/users/fpvandoorn/following{/other_user}","gists_url":"https://api.github.com/users/fpvandoorn/gists{/gist_id}","starred_url":"https://api.github.com/users/fpvandoorn/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/fpvandoorn/subscriptions","organizations_url":"https://api.github.com/users/fpvandoorn/orgs","repos_url":"https://api.github.com/users/fpvandoorn/repos","events_url":"https://api.github.com/users/fpvandoorn/events{/privacy}","received_events_url":"https://api.github.com/users/fpvandoorn/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":0,"created_at":"2015-04-04T02:18:22Z","updated_at":"2015-04-04T02:18:22Z","closed_at":null,"body":"In [this gist](https://gist.github.com/fpvandoorn/a645917ca52129319fd8) the rewrite tactic fails on line 132, even though I give the complete pattern. \r\n\r\nWhat is even stranger: if I copy-paste the whole goal to a new example (lines 136-147) and apply the same tactic, it does succeed. It somehow seems as if an earlier tactic did something strange to the proof state, which makes the current tactic fail. \r\n\r\nThis also happened in #488. I've had this a couple of times earlier, with either `esimp`, `rewrite` or `clear`. However, it makes it hard to create a minimal example, because I need earlier steps of the tactic proof as well.\r\n\r\nI hope you forgive me for not making a minimal example because of this."}}