Requirement for being @[simp]

Stream: general

[Yury G. Kudryashov]

Hi, what lemmas can (not) be marked as @[simp]? In particular, why arrow_congr_comp_apply in https://github.com/leanprover-community/mathlib/pull/1119/files can't be marked as @[simp]?

[Yury G. Kudryashov]

ping in this topic

[Floris van Doorn]

You should think of simp lemmas as reduction lemmas from the LHS to the RHS. In particular, given an instance of an LHS I need to know what expression (the RHS) it will reduce to. This is not the case for your lemma, since eb occurs in the RHS, but not in the LHS.

[Yury G. Kudryashov]

@Floris van Doorn Thank you for the explanation!