mathlib3

ad588611 - refactor(group_theory/submonoid): adjust definitional unfolding of add_monoid_hom.mrange to match set.range (#7227)

refactor(group_theory/submonoid): adjust definitional unfolding of add_monoid_hom.mrange to match set.range (#7227) This changes the following to unfold to `set.range`: * `monoid_hom.mrange` * `add_monoid_hom.mrange` * `linear_map.range` * `lie_hom.range` * `ring_hom.range` * `ring_hom.srange` * `ring_hom.field_range` * `alg_hom.range` For example: ```lean import ring_theory.subring variables (R : Type*) [ring R] (f : R →+* R) -- before this PR, these required `f '' univ` on the RHS example : (f.range : set R) = set.range f := rfl example : (f.srange : set R) = set.range f := rfl example : (f.to_monoid_hom.mrange : set R) = set.range f := rfl -- this one is unchanged by this PR example : (f.to_add_monoid_hom.range : set R) = set.range f := rfl ``` The motivations behind this change are that * It eliminates a lot of `∈ set.univ` hypotheses and goals that are just annoying * it means that an equivalence like `A ≃ set.range f` is defeq to `A ≃ f.range`, with no need to insert awkward `equiv.cast`-like terms to translate between different approaches * `monoid_hom.range` (as opposed to `mrange`) already used this pattern. The number of lines has gone up a bit, but most of those are comments explaining the design choice. [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60set.2Erange.20f.60.20vs.20.60f.20''.20univ.60/near/234893679)