As far as I can remember, idi was *inserted* by 'minimize' in some cases, and I had to remove it manually. Unfortunately, I do not know when and in which context this appeared, but I think the concerned theorem was not marked as "usage discouraged"... Maybe there was an error which was fixed meanwhile - I will come back to this if it happens again.
Looking for idi in the current version of set.mm, there are a lot of "idi"s in the proofs of the theorems Glauco provided in December (in his mathbox)! Since they are very long, I fear that 'minimize' will take a long time to run. I tried it with a smaller one (~fourierdlem12): 'minimize' ran some minutes, and decreased the proof from 4678 to 4474 bytes, 11567 to 10757 steps (567 to 520 essential steps). "idi" was removed by this minimization, so everything is fine. -- 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/061e1d36-8146-4e85-80d6-c3f849c2826b%40googlegroups.com.
