mathlib3

28f7172e - refactor(algebra/direct_sum/basic): use the new polymorphic subobject API (#14341)

refactor(algebra/direct_sum/basic): use the new polymorphic subobject API (#14341) This doesn't let us deduplicate the lattice lemmas, but does eliminate the duplicate instances and definitions! This merges: * `direct_sum.add_submonoid_is_internal`, `direct_sum.add_subgroup_is_internal`, `direct_sum.submodule_is_internal` into `direct_sum.is_internal` * `direct_sum.add_submonoid_coe`, `direct_sum.add_subgroup_coe` into `direct_sum.coe_add_monoid_hom` * `direct_sum.add_submonoid_coe_ring_hom`, `direct_sum.add_subgroup_coe_ring_hom` into `direct_sum.coe_ring_hom` * `add_submonoid.gsemiring`, `add_subgroup.gsemiring`, `submodule.gsemiring` into `set_like.gsemiring` * `add_submonoid.gcomm_semiring`, `add_subgroup.gcomm_semiring`, `submodule.gcomm_semiring` into `set_like.gcomm_semiring` Renames * `direct_sum.submodule_coe` into `direct_sum.coe_linear_map` * `direct_sum.submodule_coe_alg_hom` into `direct_sum.coe_alg_hom And adds: * `set_like.gnon_unital_non_assoc_semiring`, now that it doesn't need to be repeated three times! A large number of related lemmas are also renamed to match the new definition names. This was what originally motivated the `set_like` typeclass; thanks to @Vierkantor for doing the subobject follow up I never got around to!