Defering a proof?

Stream: new members

[Sorrachai Yingchareonthawornchai]

Do I understand correctly that we must immediately prove the statement in ' have' tactic? Is it possible to state a claim and use it to prove other lemma and then later prove the claim?

[Edward van de Meent]

you can do have h : True := ?procrastinate

[Edward van de Meent]

which adds the proof of the have-statement to the list of goals, but you can prove that in whatever order you'd like

[Edward van de Meent]

if at some point you'd like to resume the proof, you can use case procrastinate => _

[Edward van de Meent]

do note that things you prove after the have don't get added to the context of the procrastinate goal

[Mario Carneiro]

you can use suffices instead of have, this inverts the order of the main goal and subgoal

[Sorrachai Yingchareonthawornchai]

thanks