use previous lemma and current hypothesis

Stream: new members

[Michael Beeson]

Suppose I have already proved lemma23: \all x (p -> q) for some complicated p and q containing x,
and in my current proof state I have h:p[x:= t], so I would like to have Lean generate for me
have h3: q[x:t] := lemma23 x h
without me having to type out q[x:=t], I just want to say, "use lemma23 on h" and have
the new hypothesis appear.
Is there any way to do that?

[Bryan Gin-ge Chen]

If I understand what you're asking, type ascriptions are usually optional, so have h3 := lemma23 x h should work as well.

[Michael Beeson]

Oh! Well, that was easy! Thanks.