chore(*): clear up some excessive by statements (#12570)
Delete some `by` (and similar commands that do nothing, such as
- `by by blah`
- `by begin blah end`
- `{ by blah }`
- `begin { blah } end`
Also clean up the proof of `monic.map` and `nat_degree_div_by_monic` a bit.
