reusing hypothesis shown in previous fields

Stream: new members

[Calle Sönne]

Hey, I am trying to show that a certain functor is full. The definition of a full functor in mathlib requires me to first provide a preimage, and then to provide a proof that the preimage is indeed the preimage (witness). Now in the process of constructing the preimage, I use Classical.choose h, where h is some quite specific hypothesis I show during the proof. Now, when proving witness I want to use Classical.choose_spec h, but this requires me to reprove h. Is there some way I can avoid this and use h again without having to reprove it? My h is quite specific, so I don't think its worth adding as an auxillary lemma (unless this is the only way of avoiding reproving it).

[Yaël Dillies]

Can you do have h : type := proof before the constructor?

[Calle Sönne]

Yaël Dillies said:

Can you do have h : type := proof before the constructor?

Oh that would probably work, didnt think you could even do that :sweat_smile: Thanks!