Commit 2022-03-10 19:33 6fdb1d5d

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.