chore: robustify for byAsSorry (#6287) This PR makes some proofs more robust so they will still work with `byAsSorry`. Unfortunately, they are not a complete fix and there are remaining problems building with `byAsSorry`.
This is the repository for Lean 4.
See Setting Up Lean.
Please read our Contribution Guidelines first.
See Building Lean (documentation source: doc/make/index.md).