Minimized theorems previously depending on df-clel, but not ax-8

[GinoGiotto]

Fixes #3402

The set.mm version preceding #3389 contained 7922 theorems dependent on df-clel but not ax-8. This PR is the result of a minimization scan of only those theorems. To my surprise this activity only took one night, which is relatively short.

The command executed is the standard MINIMIZE_WITH * /ALLOW_NEW_AXIOMS * /NO_NEW_AXIOMS_FROM ax-*.

In the whole set.mm only bj-ax9 and bj-ax9-2 used to depend on df-cleq but not ax-9, so there is nothing to minimize there.

Some theorems in the set.mm version preceding #3389 used to have different names than now, so after minimizing I collected the ones generating the error ?No $p statement label matches <label> and rescanned them with their actual name.

Some thoughts by looking at the changes:

• I suspect wl-dfclab was meant to have a "proof modification is discouraged" tag (maybe bj-epelg as well?).
• Theorems abeq12 brabg2a iunxsngf2 rabeqd fnfvima2 seem to be redundant.

The full comparison in axiom usage can be consulted here: 3d9d2a0.

NOTE: The reason commits skip from min1000 to min3000 is because min2000 didn't show any result.

[avekens]

There seems to be some redundant theorems now (minimization resulted in one-line-proofs). These should be consolidated (one of them to be removed, the contribution information must be aligned).

[avekens]

Some thoughts by looking at the changes:

* I suspect `wl-dfclab` was meant to have a "proof modification is discouraged" tag (maybe `bj-epelg` as well?).

* Theorems `abeq12` `brabg2a` `iunxsngf2` `rabeqd` `fnfvima2` seem to be redundant.

OK, then my review remarks are already known. About wl-dfclab, @wlammen should decide, the other 5 theorems should be consolidated.

[GinoGiotto]

@benjub what do I do with bj-epelg?

[benjub]

@benjub what do I do with bj-epelg?

It should have the "proof discouraged" tag, but if it's easier for you, don't worry, leave it like that and I'll restore the proof later, with the tag.

Thanks a lot for this PR and the very rigorous methods you applied.

As for the absence of theorems requiring df-cleq but not ax-9, now I remember that it's because at some point, Norm proved the hypothesis of dfcleq using axext3 and not ax-ext in order to achieve that result, because of bj-ax9. I don't know if there was a global minimization since then, but in any case it's not too important, and it can wait a future global minimization.

[benjub]

I looked at some of the more significant shortenings to see if the non-minimized proofs had insight that would be lost in the minimization, but all seem good to me (and some minimizations would have occurred even before the change).

[icecream17]

feel free to delegate brabg2a to me

In fact, to avoid merge conflicts, perhaps this pr could be merged and the duplicate theorems fixed in another pr

[GinoGiotto]

In fact, to avoid merge conflicts, perhaps this pr could be merged and the duplicate theorems fixed in another pr

I fear merge conflicts too, perhaps that's a good idea, either way I promise I will commit the non-self-assigned ones tomorrow or earlier (I can't work on it right now).

[benjub]

Ok. So if we merge now to avoid merge conflicts, there remain the following TODOs:

• restore proof and add "proof disc" tag to: wl-dfclab and bj-epelg
• remove the theorems: abeq12, brabg2a, iunxsngf2, rabeqd
• fnfvima2/fnfvimad: the shorter proof and remove the other; do a second MINIMIZE_WITH *; for the label, I would choose "fnfvmiad"
• revert the "shortening" of drnfc2 and understand why the minimization made that change

[GinoGiotto]

I think I did everything TODO, as suggested I reminimized fnfvimad generating an even shorter proof.

• fnfvima2/fnfvimad: the shorter proof and remove the other; do a second MINIMIZE_WITH *; for the label, I would choose "fnfvmiad"

I suppose this is a typo, I kept the label "fnfvimad".

[avekens]

Great job! Only one minor thing:
It should be documented in changes-set.txt that the theorems abeq12 brabg2a iunxsngf2 rabeqd fnfvima2 were removed as duplicates, e.g.:

20-Mar-21 biimpa21 --- deleted; duplicate of biimpac

[GinoGiotto]

The additions to the changes-set.txt file generated a merge conflict, but I think I solved it.