Confused by "simp_nf linter" error

Stream: new members

[Sebastian Monnet]

My PR #13307 is failing the "Lint mathlib" check, because apparently the lemma inclusion_right in algebra/algebra/subalgebra/basic can be proved by simp. I can see why this is undesirable, since the lemma is a simp lemma, so this makes it kind of redundant. I have two problems, however:

1) As far as I can tell, my PR doesn't change any files that subalgebra/basic depends on, so I don't understand why the changes of the PR are triggering the error

2) I'm not sure what the appropriate response is - should I just delete the lemma that's causing the problem?

[Yaël Dillies]

This is just because I added the more powerful simp lemma inclusion_mk, which proves inclusion_right. I'm getting a PR out to add those lemmas everywhere and unsimp the now redundant lemmas. Hold tight.

[Sebastian Monnet]

Yaël Dillies said:

This is just because I added the more powerful simp lemma inclusion_mk, which proves inclusion_right. I'm getting a PR out to add those lemmas everywhere and unsimp the now redundant lemmas. Hold tight.

Okay, thanks!