A bit of a vague question but is there a tactic where I can pass in a type or prop and that gives me two new subgoals one to prove that the type/prop implies my current goal and the second to prove the claimed thing?

enough P. Or the more common assert P, which gives the same goals but in the other order: first prove P, then use P in the original goal.

Thank you as always!

Last updated: Apr 14 2024 at 11:02 UTC