backwards reasoning

Stream: general

[Reid Barton]

Can someone remind me of the status of backwards_reasoning in mathlib? Is it still in PR limbo, or did it get merged into solve_by_elim, or what?

[Scott Morrison]

It is in limbo, waiting for me to respond to reviewers' comments. I have been at a conference all week (for which I'm an organiser, and which has been full of interesting maths), so haven't touched it. I'm also realising I should be doing more maths and less Lean...