B C_ A( ~ undif ), or in this case
~P A C_ ~P ( A U. B ), which you would have to get from probably ~ ssun1 and ~ sspwb; Norm always likes shorter versions of proofs, and this seems like a relatively easy one to put together
The stake is this: I shouldn't need to write down more than the essence of this argument (see also reccot), which is
In the context |- ( ( A e. CC /\ ( sin ` A ) =/= 0 /\ ( cos ` A ) =/= 0 ) -> ... ) , we have ( 1 / ( cot ` A ) ) = "by (cotval)" ( 1 / ( ( cos ` A ) / ( sin ` A ) ) ) = "by (recdiv) using (sincl) and (coscl)" ( ( sin ` A ) / ( cos ` A ) ) = "by (tanval)" ( tan ` A )
All other steps that are needed, are fully generic rules for transitivity, "windowing" rules (here: oveq2d used in the first step), context manipulation rules, and commutativity rules (not in this specific proof). Automation should be able to find those steps.
set.mmproofs so that the calculational (or arithmetical, or whatever) essence of the Metamath proof is kept, in such a way that that essence can also be used in other ways and by other tools.
#lang mmcalc?) which allows import
set.mm, parsing it using specific
$j-like rules, and then give a calculation like the one above, and then e.g. output the resulting proof to a .mm file.
I've been thinking about something similar for a long time. I work primarily with lean now, and the "plain proof" mode there includes the concept of a
calc block, which would look like:
calc 1 / cot A = 1 / (cos A / sin A) : by rw cotval ... = sin A / cos A : by rw recdiv ... = tan A : by rw tanval
which is clearly very similar in spirit to your version. I've wanted a proof interface for metamath in lean for a long time now, and some recent developments are making this more practical, but it's certainly a long term project with no completion date right now.
sbcex2and its universal counterpart)