Unused fintype in type linter

Stream: mathlib4

[Thomas Murrills]

I'm starting to fix unused fintype assumptions in #31795. However, I noticed (a little late!) a note on #10235 asking that failures related to HasFDerivWithinAt.pi not be fixed, as these finiteness assupmtions will be unnecessary after a port to TVS.

@Yury G. Kudryashov, how many/which files does this extend to? Many declarations seem to have something to with derivatives and pi-types here, with many downstream declarations, and I'm wondering if they're all related (or if this is meant to be much more narrow).

[Thomas Murrills]

@Yury G. Kudryashov Just pinging you again for when you have time, in case you missed this. :)

[Yury G. Kudryashov]

Sorry for the delay. I think it's OK to fix it now. I'll remove the assumptions when I have time to work on the derivatives over TVS.