Tactic Wish: rw [..., ?]

Stream: lean4

[Tristan Figueroa-Reid]

[I hope I am not alone in this] Sometimes, when writing a theorem, I use rw? to get a feel of the environment again - when doing this, I (not rarely but not commonly either) sometimes notice exactly how to prove a part of a goal with just rewrites. It would be nice if there was a way to chain these rw? guesses together instead of having to type rw? again on the next line. For example,

theorem test := by
   rw [existing_thm, ?] -- it would suggest a secondary rewrite on top of the current one.

[Yaël Dillies]

@Jovan Gerbscheid's rw?? tactic will hopefully be reimplemented so that one doesn't need to write anything more

[Jovan Gerbscheid]

Yes. I was still kind of waiting for the discrimination tree PR to get merged before polishing up the rw?? PR. I will soon finish going through the former with @Anand Rao Tadipatri.