an approach i'm finding increasingly productive is to break up a proof into parts i "obviously" believe to be true and shim them with `sorry`s, focusing on the rest of the argument. i'd previously always write top-down but now i just leave those unsolved and come back when the big picture is clear