All that needs to be checked to avoid that is the statement of the main theorem. Any divergence further inside means you proved the main theorem differently than you thought you did -- but you still proved it.
This assumes the Lean kernel itself isn't bugged, but getting it correct is a matter that affects all uses, not just this one, so the cost of making it correct is spread over all those uses.
This assumes the Lean kernel itself isn't bugged, but getting it correct is a matter that affects all uses, not just this one, so the cost of making it correct is spread over all those uses.