Debugging instance non-matching

Stream: new members

[Yakov Pechersky]

I have a case where rw or similar tactics aren't working on a goal I would think is identical to a hypothesis I have. What are the best tools to see what is going wrong, other than starting at the output of pp.all?

[Eric Wieser]

Build your proof in the reverse direction until you get to the state you're stuck at, and then use convert to match up the things you expect to be equal?