[yccs27]

This is the crucial insight. The last proof in TFA writes it in differential form notation, where "dx at constant y" is dx∧dy = -dy∧dx.