Found it: https://groups.google.com/g/metamath/c/2AW7T3d2YiQ/m/iSN7g87t3ikJ
On Tue, Aug 11, 2020 at 3:48 PM Mario Carneiro <[email protected]> wrote: > This fact was being deliberately not exploited, for reasons that I forget, > possibly involving type hygiene or something. I think Norm made the call on > that so perhaps he can recall better. > > Mario > > On Tue, Aug 11, 2020 at 2:20 PM 'Alexander van der Vekens' via Metamath < > [email protected]> wrote: > >> That's really cool: I think you are right with your assumption that the >> number of hypotheses should be as small as possible, and ~xrltle >> could/should be revised accordingly (in my opinion). Unfortunately, I >> cannot see your proof for ( A < B -> ( A e. RR* /\ B e. RR* ) ) (the link >> goes to a site for which I have to provide login information), but I guess >> you use ~brel to prove it. >> Of course such a change will have an impact on existing proofs - they >> should become shorter. ~xrltle is currently used 65 times. I do not know >> if the minimize command will replace the current version as soon as the new >> version (without hypotheses) is avaiable. >> >> On Tuesday, August 11, 2020 at 5:36:57 PM UTC+2 [email protected] >> wrote: >> >>> I've been playing around with the OpenAI assistant too, thanks so much >>> Stan and Auguste for letting me use it. It did something weird the other >>> day which was surprising to me and I imagine everyone else knows this >>> already but I wanted to ask what to do. >>> >>> It proved this >>> <https://mmproofassistant.azurewebsites.net/#eJyNU91vmzAQ/1csPzUTySAMRlA0aaEvq1Rp4qlSGk0GnGDi2gxM2izjf5/Nx+w0S7QHpLuzud/H+U6QCPxSw/AE3/iiCNxEUJWIY4lhCClKMIUWLFGFmYAhayi1YC2Q/KkrQCrIS1lheYdkMtVNLEg5ygjbwXCLaI1bC+6zgnxaBIeDgZDhOq1IKQhnN3HuIs5ERZJG4AwkR/DAGfiOGUNMWMCbPjR0Orfn9mwyMtFgErkuXbHIqG8i58eSixzXpL4JPPbTLfrzRpoGU8prnCmEw3afp/ucZQbCjqPb5t2Br2AJVmD6BagQz0AcfwAfn59lbUgmYHJhpQVTTikqFfRY6ThqEgZHXmKmGDpkFxQ/X18Lg6FAqSCpwfGixUh1vQa/pyAG0Q9JNQJPM3AvuW02qqq4x2cyIi1CXZuA00kehPJrWxWvZLwa4kjGSmmf3Z9lscyWMlYWdE8xhEnVvchOr5b0Xq8cCKKNlGjPFnbgO599d+54dhDYvrTC9ci2EL4rrg/rovdoxLK3QHF8Gkb0/wPSwP8YkOc5/v4XSfObA3rfwhhQP40rBAf7qJD+vVWjgxrzqoNO26rfj7yRMOuzDdc7Zp3th/mITB9N7hp5Yw0yv7Gy+bsnZcX59vGxT9s/lAtvBw==> >>> ( >>> A < B -> ( A e. RR* /\ B e. RR* ) ) as part of a proof, which I found >>> surprising. The main idea is < is defined on the reals, ltrelxr >>> <http://us.metamath.org/mpegif/ltrelxr.html>. >>> >>> And so I have ioounsn <http://us.metamath.org/mpeuni/ioounsn.html> in >>> my mathbox which is stated as ( ( A e. RR* /\ B e, RR* /\ A < B ) -> ( ( A >>> (,) B ) u. { B } ) = ( A (,] B ) ) but using this trick above I managed >>> (well mostly the assistant managed) to prove ( A < B -> ( ( A (,) B ) u. { >>> B } ) = ( A (,] B ) ), here is the proof >>> <https://mmproofassistant.azurewebsites.net/#eJzNW22P2roS/isRn+CK3Zv3l9X2SrD9co901HbbqpV6qlVIAgTyAiQBkp7+9+u8euIYQ1h6T1WpskN2/Iyf8cx47PwYuLHjR4OHH4NjaKx0aRZ7eSdON87gYeCZM8cbjAcbc+cE8eAhSDxvPIhiE/1R8WDghmESRIEtordcGz3AYsYDLzRtN1gMHuamFzk/x4O1vXJlQ9/vwRi2E1k7dxO7YcAcafgUBvHOnSWxY3OzlPsjDLj3ThCYQTzmlLs/Eu9O5EX+flQjwYOhkffz9dJaLwMbjLwITbZyQ26z5O7+ww3Rvwk3HI+4KTfiknvuB2r8RM031Q/fix9GHZXHAyv0PHMTOXbzpMCG4ZQjJoiCQbhxghxrrPPLWDxoAcC6TDdhvHQiN7oI8YR7zCHVU4ElguEsL8xxoQEFU0gDJdiIYMDYtGLXAoN1MNdjfvvG/X3H4ZHfFJMBHk3Royf06Pt38sX86Y8fqPlweo5//sxfeSpewXNdPkWSHvL/yt6UJmaIGt9qgtCLOUeFVT8MnG28s+spwnNAMoKMx/QSNCf8vaQKgqLJsqDpvKKoMpq7TFBlzZGzxWnD6sjuZV9MfXqYHAZKMbnoYEeaw/viLbVoQ716rWBsFODp3HJsd3UwmaZL6s423badDpHtIWUmlQpFp9SostySLGiCWG3SeEdU4wU2mQTOVmyMEmvHMEpZ52VNlxRZlDRJkKTcg6SbuRk4icmgk5RN0lmq9abN4uWsYQgU1mTLsldaGgdM1kgRfVjLfc4EeheSkynBHJUNZ2uFfsMGRs1gw1B5STF0SVVUQRJFAWm7ne1nlmXJMYMNUnZ3cWEF3tT+4XI2MAQKG+ousHcB8uxMNkgRdDY2UeP7o7xvLTvUFI/QjFtLgpg3JwgpehHqTTnnnnt+/lebpCj1aoawJiyGdElQRF1FLAmSJuQM7RNt7QpKKy8hGSJlY4YaWK/nCQOh8BTaibu2j6bNDtOECMBTzcOkBXhSAJ5UgCdF4KmWzbQ9065luc1qwGhOznU+tbPgKKy2XjBjgiZ9/FnjwpYE+nHTL8zv33/9hRropbxR/DYq3jI7Jlk86tgceno2oWhHNWCrYJbz4afUTv0XxVIoc7Zq6GUx+48vJAXI2AXRDKyaBTy9DItXROSKkENCWYsmaHweIeTFIlYsP0kYFk/K7vqki1TsYf4YFcX8HVM5OI6asdzoOcjVlPaAhEelZeqzuSYG1mJ3FaThpTNYGnJpH+VPpRalPf+qvAsrR4sZfJJGSRYf2BGcENHonkM6cEcu5TJuNOKGOeR2/4nov0P9svW+aX1oWs+tdz+2ep9avc+t3pdGwteyVTqcd8WsHWsGxugvqubfRWaUNd3itWf0IOclQyOn+aIu3dD7flI+NVI+QylDbtg2jAM2jCrgfELPHlH77h41Pla8oz/9cK0aHQCHk2b6RKAZVhDKF78WWzz0wwHJfKpxsQ2f1C9/90sjMdd1VOZ9z0UT+3K22KfuevpC4AQDvoOL6X31a7mUPlS9KkZOQEI5BQl/3X6XB4Nx7enfo16+Nsveh+K3uveMeo9V+yNof8rbL1XnM+x8AW99hT8cUCer2kfUPlbtFLXTqp2hdkIE+OMxCZpkqlnijNCiy2j7ociaqmuGpmrIM5grZS7NopnOyqUI0Y1fGI/OmGzSNtlH9CBnMEGtymQvd3AYKcXBeXtzryWb3foKNXKC+6nxgvV46a8IxkpRhLf8Nb87HFlh8yQfpO/JOr4H4c1q55OVVac+0DE6CnQ9XXjifiX4V5lSXw5eRQGGStFDW678WPZn6ZUUZCed2rTjK7NuloB+yZqM4XKVMGqKSlvZlpdHXmTumBgqnfbTpIl1Ep+s9v+PRbPPLrgBTatJ6OnaiISdwMxoSJ8BMpomr8A7rbPuLCNtsI7AjTvr6cHt+Z0bhk3FotGJuUeT/VUki2rGLqKRXoap+nkXSKr+gnV/eYXyVrM1wloxlU9SL4y3M9lnKk/6Kcqu+pRRj+q9UrEEK1eJGsWWu7XVrtOIrK3Wcec5gRfXemHA7I333FrFVqpaTL1Iv3XGnvuSehtOQ7zdbZRi6q5mByEys1BlV7QId9CDU3rmSziqJ+yoLsoYu7THnhPvmnysUYqp+97V9qa+X7IPc0jnTi+4tKp43cJ4U2Upiiv4vbqikdUFjKa2cmEsA3WU7JKqiGmbATjLwVPAyFw1lLFKgiyroiHymqyjqfN1XbP5ucjK+UjZ18XpUqsrAzOGSQljgryzt0YUsjfmpAiS/oLjHHhRciPruPDXDv24sttVElhCM1f0+i6gm1bzlQrGpZpwrDSr7quJMuJbEWTV4GUlP7wLI9vfWFuBcSrckX2e8FtwjJFRODZi3tQ03QiZHJMirgpZpQYTXHCqfFhG+LCO36qpwViZXktQlTmvLII1UyWyPviKMjHpyypTbleLa1smDJNyNDG53HRXltnYbaM101HpqiDzMnJWhqHLKpqtQxxm6fZgGSy7JWR3rwjUZF9ulXhc2i5nK5iqG8fCK0BNrwCFx6Vt42eGkonL8orL/xEUHpe2JV/w21RKA3bKSU42I0RXltuN0cVSuMqK4ZmD62+8Jrhi8CxfK2qSguxWM1B4lfXcZueHzBMifcZigpR96YlDL9eKgVCoOXqubluZtGBSQ4q41VnoKe0YhD1STohqqrAyrAqezhuGwou6KEi8ouaHQ1kQKYkaH1m3QUjZmKomatyELYyFwpatSoKwjiOZffuDENFm65l7einudXy9594CgvL6MlTjCSvx9pJsHi+0t61eXeUFlM12TsMZVom1vGRdUGSZV2SDl6TiHpLvxkbmrXZzBmek7HoiHsspyDF+7e3p8MAUgubH7HCMfHXPzkYJEZ1M5QTAavq8GM3fsdkn4TGZGYeoHuauNre27H0SEVyuccKtRf4aJ4x3OBh8PyfMu4dYEdM5ywmTsn+JE8ZAaIeLc4NXFV9lX0ghRfRIBk8nf1dnfYAqkOBhTVgeWNEUUURuWFMkVdXznajsqkdL9A1m5ZuQfYsED49LocV1Asl1JXX1ClDX5FJ4XNp+17fTpaFpN7aVfyZgY2XOB2zFkHlVkgUDTcIqiNeBFoUscyFl/6qAjbHQ4sEqNUwtlFwmW6SI3zpgY5X6Bey1PzNWx/nCY3BGyr5JwMYDUwjazbdSIrqawiSIFPG6gI3HZAZsQ1zq+yzW2EVd8r7ObVb6tFPJ7HkzEYNnrWxNkhRFFzVD03ldyVe26lu7XSR4S4aVkLJv4XPxuNT4fNQXnhqxrj2dBgWvS/a/j4XHpgBbi5nirxRHYpoIKeLMDcmi+AXuEnfLXQ6+FYkRMG3Zmq2C41Kz2FGLJOE3ST4x+H7JZ5KstslGnlkMsyFl/5LkEwOhXTrYbmapo/vs4iop4jdNKLAy/SoAwtpcqta8dYpAUkXK/lUJBcZC+/4jMebH1DywTzl7s/UPbBWwJv22ClIW8+tD7LPOMEjZt9gq4HEptCyX+s4VNYt1vfgcqGvCFh6XAso3g5Wo2pHHtBXS3H7r5BOr1C/51BaGHobRnvXVGin7JsknHpiWfAq24CzDzYZdkiFEvDL5bMZkBOz8IMFMwwQN8631hSv+xnTc+sgSfisJv5uDH6LBD7Dgp07wUyD40Q38AAV+5NH6EAN8RwEvnsODM3jcAc8YYPEdFrhhpReWUmE1EVbwYP0Nls9gXQnux+HGFO784OYHbjjgdgGWG2DtApYM4FEM3B3ADBVmWjAFgYEDxjvoJOA6gbYJLQv6Oug4ob+CaSlMI+ElenilDl5Fgxe94D0teAcKXmGCd4jgFSB4vwZeEYG3HuDdAXg4Ds+b4akvvGaD77B8H1dL+7/BJl9X5bfMm10Yzv/8s+z+/B9p9hyj> >>> . >>> >>> So I guess my questions are firstly is it good form to reduce the number >>> of hypotheses? Does this have implications for other proofs in the main >>> body such as xrltle <http://us.metamath.org/mpeuni/xrltle.html> or it's >>> nearby theorems. I think there must be a lot which state A e. RR* /\ B e. >>> RR* as well as A < B in them. I guess it doesn't matter because A e. RR* >>> isn't constricting the theorem at all, it's just a redundant statement so >>> maybe it is irrelevant. I am not sure if anyone else is interested but I >>> thought this quirk was cool. >>> >>> Also as a side note is it ok to upload deduction versions of the >>> theorems in my mathbox? I don't want to have too many copies of trivial >>> things in there. It's a bit hard to replace what I have as I've already >>> used them in later theorems, though maybe changing them too is not >>> insurmountable. >>> >>> -- >> You received this message because you are subscribed to the Google Groups >> "Metamath" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected]. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/metamath/24949dad-3d5b-4a94-b5e4-4d8c01ff74b7n%40googlegroups.com >> <https://groups.google.com/d/msgid/metamath/24949dad-3d5b-4a94-b5e4-4d8c01ff74b7n%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSvm%3Dcgr2-LBvrq-dhGRV5u-vVpvPmqn9OLn_QmPS-ssmQ%40mail.gmail.com.
