chore(analysis, measure_theory): Fix lint (#16216)
Satisfy the `fintype_finite` and `to_additive_doc` linters. Further, perform the similar weakening from `encodable` to `countable`, even though that's not yet linted for. The advantage of this is that `finite α → countable α` in known to TC inference, while `fintype α → encodable α` is not (because it's noncanonical data).
As a result, some lemmas that were proved for both `fintype` and `encodable` are now deduplicated.
