Commit 2025-01-10 04:26 5ce9aa28

chore(Algebra/Lie/DirectSum): shorten proof of lieAlgebraOf.map_lie' (#20592) Uses the lie_of_same lemma added in #8388 to shorten a 13-line proof down to a single line, removing two erws and one porting note. According to set_option trace.profiler true, the new lieAlgbraOf declaration takes 135 milliseconds to elaborate, compared to 298 milliseconds for the declaration it replaces. Found via tryAtEachStep.