Zulip Chat Archive

Stream: new members

Topic: use previous lemma and current hypothesis


view this post on Zulip Michael Beeson (Sep 05 2020 at 15:40):

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?

view this post on Zulip Bryan Gin-ge Chen (Sep 05 2020 at 15:42):

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

view this post on Zulip Michael Beeson (Sep 05 2020 at 15:42):

Oh! Well, that was easy! Thanks.


Last updated: May 17 2021 at 22:15 UTC