Commit 2025-01-10 06:07 8448d4bb
View on Github →chore(GroupTheory/CoprodI): shorten proof of lift_word_prod_nontrivial_of_not_empty (#20587)
Replaces 9 lines of proof with a single application of lift_word_prod_nontrivial_of_other_i.
I observe this change to speed up the time reported by set_option trace profiler true from 280 milliseconds to 140 milliseconds.
Found via tryAtEachStep.