Commit 2026-11-10 13:26 c2c597b4

chore: golf some conv proofs (#45393) This PR golfs many conv proofs. This is in preparation for #45124 (multigoal linter in conv). I used enter for these golfs and not arg/lhs/rhs/ext, because enter supersedes all of these. Some of the golfs are not required by the new linter, such as for proofs that look like

congr
· skip
· rw [...]

But this can be cleaned up nonetheless.