Formally verifying digital circuits with category theory in Lean