mathlib

f44a5eb1 - feat(category_theory/concrete_category): id_apply, comp_apply (#7530)

feat(category_theory/concrete_category): id_apply, comp_apply (#7530) This PR renames * `category_theory.coe_id` to `category_theory.id_apply` * `category_theory.coe_comp` to `category_theory.comp_apply` The names that are hence free up are then redefined for "unapplied" versions of the same lemmas. The `elementwise` tactic uses the old lemmas (with their new names). We need minor fixes in the rest of the library because of the name changes.