Feel like “translating the proof into your end product” is a bit of a “draw the rest of the owl”

You assume lean can express more than it can.