the json file next to the problem statement in lean says the solution starts here: https://github.com/openai/math/blob/main/lean/OAI/Combinator...

the proof is probably split over the constructions in the whole directory.