unnecessary(?) simp lemma

Stream: general

[Yury G. Kudryashov]

I wonder why submodule.map_subtype_top is not reported by lint.

[Yury G. Kudryashov]

The proof is by simp

[Gabriel Ebner]

We have quite a few of these "short-circuiting" lemmas. It's not redundant because simp will actually use map_subtype_top preferentially. The lemmas used to prove it are not redundant because the don't follow from map_subtype_top.

[Yury G. Kudryashov]

Thank you for the explanation.