bug in unusedHavesSuffices linter

Stream: mathlib4

[Sébastien Gouëzel]

I think I've just encountered a bug in the unusedHavesSuffices linter, in #19696: it complains that two lines should be removed, but as far as I can tell they're necessary. The situation is unusual enough that I'm not surprised the linter is confused: a typeclass ContMDiffManifoldWithCorners I 1 M is necessary for the statement to make sense (it is required to endow the tangent bundle with a topology), but it can not be found by instance search, so I give it with haveI in the statement (so that the statement makes sense), and then again with have in the proof (so that the proof makes sense). The linter complains wrongly that I should remove the ones in the proof.

I have a "fix": use also haveI in the proof, instead of have. But it doesn't feel right.

[Ruben Van de Velde]

Odd. I think it's also fine to just disable the linter

[Junyan Xu]

I observed the same here and the haveI fix also works. Interesting that the linter doesn't flag mapPiLocalizationIsMaximal_comp below on line 326.