I feel sorry for whoever has to read and understand the solution. It looks like the typical convoluted unreadable mess I see the models generate for software. It might be technically correct, but gaining insight from it is just intellectual hell.
Skill issue. Also lean is meant to be executed, not read.
There's an opportunity to build a Lean "optimizer" which automatically simplifies existing proofs.