Rewriting inline

Stream: new members

[Jérémie Turcotte]

This might be an elementary question, but how does one rewrite (substitute) some equality in a line without taking a new line? Say, instead of doing have "temp:=something, rw h at something,"? I find I often find myself writing too many lines for nothing

[Matt Diamond]

someone might have a better answer, but one solution that comes to mind is foo := h ▸ something (using the infix version of eq.subst)

[Matt Diamond]

that only works in certain cases, though

[Jérémie Turcotte]

Yeah, I tried that, but (at least in the place I'm trying to use it now) getting error "invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables"

[Junyan Xu]

I'd also try h.subst (if rewriting from left to right) and h.symm ▸ and h.substr (if rewriting from right to left) before giving up.

[Marc Masdeu]

I like to use the following: rw [show foo, by some_tactic] at bar when I want to avoid a have. It's not exactly answering the question, but it saves lines in similar situations.