Commit 2025-02-21 13:51 8d88c000
View on Github →chore: more renamings to fit the naming convention (#22148)
By the naming convention, a lemma about Sum.map should have sumMap in its name, not sum_map, etc.
Rename sum_map -> sumMap, sum_inl -> sumInl, sum_inr -> sumInr, sum_casesOn -> sumCasesOn as appropriate.
Together with #22155 and #22156 (which are disjoint from this), this is exhaustive.