simp normal form linter error

Stream: mathlib4

[Calle Sönne]

I am getting the following error in a branch of mathlib (linter complains that simp lemma can already be shown by simp)

Error: ./././Mathlib/CategoryTheory/Bicategory/LocallyDiscrete.lean:113:1: error: CategoryTheory.LocallyDiscrete.id_comp.{v, u} simp can prove this:
  by simp only [CategoryTheory.sum_comp_inl, CategoryTheory.sum_comp_inr, @CategoryTheory.Category.id_comp]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].

Here is the lemma:

@[simp]
lemma LocallyDiscrete.id_comp {a b : LocallyDiscrete C} (f : a ⟶ b) : 𝟙 a ≫ f = f :=
  Discrete.ext _ _ (Category.id_comp _)

I tried using the suggested by simp only [...] as in the error, but it doesnt seem to prove this lemma, and neither does simp. How do I avoid this error? It suggests I move the lemmas around in the file and/or add @[priority], but I don't see how that helps since simp doesn't prove the lemma anyways.

[Calle Sönne]

For context this is on the branch callesonne_locallydiscrete

[Joël Riou]

It is provable by simp once you have obtained the instance Strict (LocallyDiscrete C).
A priori, I would suggest moving the proof of these three lemmas id_comp, comp_id, assoc to the definition of this instance, but you may remove them completely, and remove also the definition of the three fields of the instance declaration because automation is able to obtain them all.

[Calle Sönne]

Joël Riou said:

It is provable by simp once you have obtained the instance Strict (LocallyDiscrete C).
A priori, I would suggest moving the proof of these three lemmas id_comp, comp_id, assoc to the definition of this instance, but you may remove them completely, and remove also the definition of the three fields of the instance declaration because automation is able to obtain them all.

I see, thanks a lot! Is it preferred to rely on automation for Strict (LocallyDiscrete C), or should I copy these proofs to the corresponding fields when defining the instance (since I have the proofs without automation anyways)?

[Calle Sönne]

In other words, should I use the automation because that gives me fewer lines, or should I copy the proofs over, which might be faster compile-wise.

[Joël Riou]

Here, I would rely on automation. In category theory, many proofs are automated by aesop_cat. In many cases, it is just ext; simp.