Lean4
/-- List of simp lemmas to apply to the elementwise theorem. -/
def elementwiseThms : List Name :=
[ -- HasForget lemmas
``CategoryTheory.coe_id, ``CategoryTheory.coe_comp, ``CategoryTheory.comp_apply, ``CategoryTheory.id_apply,
-- ConcreteCategory lemmas
``CategoryTheory.hom_id, ``CategoryTheory.hom_comp, ``id_eq, ``Function.comp_apply,
-- further simplifications if the category is `Type`
``forget_hom_Type, ``forall_congr_forget_Type, ``types_comp_apply, ``types_id_apply,
-- further simplifications to turn `HasForget` definitions into `ConcreteCategory` ones
-- (if available)
``forget_obj, ``ConcreteCategory.forget_map_eq_coe, ``coe_toHasForget_instFunLike,
-- simp can itself simplify trivial equalities into `true`. Adding this lemma makes it
-- easier to detect when this has occurred.
``implies_true]
