This PR is part of my [plan to refactor `algebra_map`](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Should.20.60algebra_map.60.20be.20a.20coercion.3F/near/297206409). It introduces new classes that should connect coercions (`↑`s) and bundled homomorphisms, e.g. `ring_hom`, so that e.g. an instance of `coe_ring_hom R S` states that there is a canonical ring homomorphism `ring_hom.coe R S` from `R` to `S`. These classes are unbundled (they take an instance of `has_lift_t R S` as a parameter, rather than extending `has_lift_t` or one of its subclasses) for two reasons:

 * We wouldn't have to introduce new classes that handle transitivity (and probably cause diamonds)
 * It doesn't matter whether a coercion is written with `has_coe` or `has_lift`, you can give it a homomorphism structure in exactly the same way.

# Additions

 * classes `coe_add_hom M N`, `coe_mul_hom`, `coe_one_hom`, `coe_zero_hom` state that the coercion map `coe : M → N` preserves the corresponding operation. They take in a `has_lift_t` instance so it doesn't matter how precisely the coercion map is defined as long as Lean can find the instance.
 * classes `coe_monoid_hom M N`, `coe_add_monoid_hom M N`, `coe_monoid_with_zero_hom M N`, `coe_non_unital_ring_hom R S` and `coe_ring_hom R S` are convenient groupings of the above classes 
 * simp lemmas `coe_add`, `coe_mul`, `coe_zero`, `coe_one`: basic lemmas stating that `coe` preserves the corresponding operation.
 * simp lemmas `coe_pow`, `coe_nsmul`, `coe_zpow`, `coe_zsmul`, `coe_bit0`, `coe_bit1`, `coe_sub`, `coe_neg`:  lemmas stating `coe` preseves the derived structure
 * simp lemmas `coe_inv`, `coe_div` (for groups), `coe_inv₀`, `coe_div₀` (for groups with zero). An alternative to having this pair of otherwise identical lemmas would be to add `coe_inv_hom` and `coe_div_hom` classes.
 * class `coe_smul_hom M X Y` stating that `coe : X → Y` preseves scalar multiplication by elements of `M`
 * class `coe_semilinear_map σ M N` stating that `coe : M → N` is `σ`-semilinear. `coe_linear_map R M N` is a synonym of `coe_semilinear_map (ring_hom.id R) M N` and also gives an instance of `coe_smul_hom`. I don't think this has any applications yet, it was mostly to test that this design would also work for more complicated classes.
 * definitions `mul_hom.coe`, `add_hom.coe`, `one_hom.coe`, `zero_hom.coe`, `monoid_hom.coe`, `add_monoid_hom.coe`, `monoid_with_zero_hom.coe`, `non_unital_ring_hom.coe`, `ring_hom.coe`, `semilinear_map.coe` and `linear_map.coe`, given the appropriate `coe_hom` class, are bundled forms of the coercion map that correspond to the `coe_hom` classes. In particular `ring_hom.coe` should become an alternative to `algebra_map`.
 * `mul_action_hom.coe`, `distrib_mul_action_hom.coe` and `mul_semiring_action_hom.coe` are bundled forms of the coercion map corresponding to `coe_smul_hom` (since they only vary in hypotheses on the non-bundled structure)

# Changes

Whenever existing lemmas had a name conflict with the new generic `coe_` lemmas, I have made them `protected`. In many places, the new lemmas are silently used instead of the now `protected` old lemmas. This caused the vast majority of changed lines. The full list is:

 * `add_monoid_hom.coe_mul` (is about `coe_fn`)
 * `linear_map.coe_one` and `linear_map.coe_mul` (are about `coe_fn` and endomorphisms)
 * `submodule.coe_zero`, `submodule.coe_add`, `submodule.coe_smul` (superseded)
 * `dfinsupp.coe_zero`, `dfinsupp.coe_add`, `dfinsupp.coe_nsmul`, `dfinsupp.coe_neg`, `dfinsupp.coe_sub`, `dfinsupp.coe_zsmul`, `dfinsupp.coe_smul` (are about `coe_fn`)
 * `finset.coe_one` (superseded)
 * `finsupp.coe_smul`, `finsupp.coe_zero`, `finsupp.coe_add`, `finsupp.coe_neg`, `finsupp.coe_sub`, `finsupp.coe_mul` (are about `coe_fn`)
 * `enat.coe_zero`, `enat.coe_one`, `enat.coe_add`, `enat.coe_sub`, `enat.coe_mul` (superseded except `coe_sub`)
 * `nnrat.coe_zero`, `nnrat.coe_one`, `nnrat.coe_add`, `nnrat.coe_mul`, `nnrat.coe_inv`, `nnrat.coe_div`, `nnrat.coe_bit0`, `nnrat.coe_bit1`, `nnrat.coe_sub` (superseded except `coe_sub`)
 * `ereal.coe_zero`, `ereal.coe_one`, `ereal.coe_add`, `ereal.coe_mul`, `ereal.coe_nsmul`, `ereal.coe_pow`, `ereal.coe_bit0`, `ereal.coe_bit1` (superseded)
 * `ennreal.coe_zero`, `ennreal.coe_one`, `ennreal.coe_add`, `ennreal.coe_mul`, `ennreal.coe_bit0`, `ennreal.coe_bit1`, `ennreal.coe_pow`, `ennreal.coe_inv`, `ennreal.coe_div` (superseded)
 * `equiv.perm.coe_one` and `equiv.perm.coe_mul` (are about `coe_fn` and endomorphisms)
 * `submonoid.coe_one`, `submonoid.coe_mul`, `submonoid.coe_pow` (superseded)
 * `subsemigroup.coe_mul` (superseded)
 * `special_linear_group.coe_inv`, `special_linear_group.coe_mul`, `special_linear_group.coe_pow`
 * `vector_measure.coe_smul`, `vector_measure.coe_zero`, `vector_measure.coe_add`, `vector_measure.coe_neg` (are about `coe_fn`)
 * `lucas_lehmer.X.coe_mul` (superseded)
 * `power_series.coe_add`, `power_series.coe_zero`, `power_series.coe_mul`, `power_series.coe_one`, `power_series.coe_bit0`, `power_series.coe_bit1`, `power_series.coe_pow` (superseded)
 * `uniform_space.completion.coe_zero`, `uniform_space.completion.coe_neg`, `uniform_space.completion.coe_sub`, `uniform_space.completion.coe_add` (superseded)
 * `continuous_function.coe_mul`, `continuous_function.coe_one`, `continuous_function.coe_inv`, `continuous_function.coe_div` `continuous_function.coe_pow`, `continuous_function.coe_zpow` (are about `coe_fn)
 * `bounded_continuous_function.coe_zero`, `bounded_continuous_function.coe_one`, `bounded_continuous_function.coe_add`, `bounded_continuous_function.coe_neg`, `bounded_continuous_function.coe_sub`, `bounded_continuous_function.coe_mul`, `bounded_continuous_function.coe_nsmul`, `bounded_continuous_function.coe_zsmul`, `bounded_continuous_function.coe_pow`,

Many `coe_` or `cast_` lemmas have been reimplemented using `coe_hom` classes and are no longer `@[simp]`. Many homomorphisms `subfoo.subtype` have been reimplemented by `foo_hom.coe`. We might consider replacing all of these outright.

Finally, some `simp` calls had to be fixed, e.g.  `simp [← something.cast_add]` could loop due to the new `coe_add` lemma, so it had to become `simp [← something.cast_add, -coe_add]`.

# Further plans

Some obvious further steps that I didn't feel fit in the (already wide) scope of this PR:

 * Reviewing for missing instances: currently I only added the obvious instances for the new classes, so we should go through and ensure everything has its instance.
 * Reviewing for missing `coe` lemmas: currently I only added lemmas that existed in the `submonoid`/`subgroup`/`subring` files, so we should go through and ensure everything has its lemma.
 * Instances for the transitivity instances `coe_trans` and `lift_trans`, so if `coe : M → N` is a monoid hom and `coe : N → O` is a monoid hom then `coe : M → O` is also a monoid hom.
 * Classes for when `coe_fn` is a homomorphism: many of the naming conflicts that required `protected` are of the form `mul_hom.coe_mul : ⇑(f * g) =  ⇑f * ⇑g`, so the obvious consequence is adding a class `coe_fn_mul_hom` along these same lines as in this PR.
 * Combining with the `algebra.to_has_lift_t` instance: this is likely to require some subtle fixing so I'd rather merge the big changes first so I don't have to keep those up to date as well.



Co-authored-by: Anne Baanen <t.baanen@vu.nl>

This had merge conflicts which I've been rather reckless about resolving. Let's see what CI says.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

This had merge conflicts which I've been rather reckless about resolving. Let's see what CI says.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

This had merge conflicts which I've been rather reckless about resolving. Let's see what CI says.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jireh Loreaux <loreaujy@gmail.com>

…f `algebra_map`

This only really scratches the surface; in general we can't afford to have two different spellings here as it forces us to duplicate every result about `ring_hom`.
A previously refactor (#17048) made these lemmas unecessary, but it was reverted to aid with the port.
Since these lemmas are needed in mathlib3 PRs, lets have them anyway.

…f `algebra_map` (#18422)

This only really scratches the surface; in general we can't afford to have two different spellings here as it forces us to duplicate every result about `ring_hom`. A previously refactor (#17048) made these lemmas unecessary, but it was reverted to aid with the port. Since these lemmas are needed in mathlib3 PRs, lets have them anyway.

For consistency with the existing `algebra_map.coe_mul` etc, these are not `simp` lemmas.
Making them `simp` lemmas makes a bunch of downstream `simp` lemmas redundant; so perhaps worth exploring in a future PR.