undetected unused instance arguments

Stream: mathlib4

[Jovan Gerbscheid]

The functions ContinuousMultilinearMap.norm_mkPiAlgebraFin and ContinuousMultilinearMap.norm_mkPiAlgebraFin_le_of_pos contain some unused type class arguments, but these are not detected by the unused variable linter, because they technically are used in the definition. In the first case, the definition starts like this:

theorem norm_mkPiAlgebraFin [NormOneClass A] :
    ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A‖ = 1 := by
  cases n

here, the tactic cases n causes all n in the local context to be replaced by Nat.zero. It does this for all variables introduced with a variable command that contain n, and thus forces these variables to be used in the current declaration, even though some of these variables are not necessary at all.

This particular case can easily be fixed, but I wonder if there is a better way to detect this kind of mistake?

[Kevin Buzzard]

See lean4#2452

[Yury G. Kudryashov]

It looks like the only way we can deal with it until hte bug is fixed is to minimize variables for each section instead of having a long variable declaration at the top of the file with all variables that will be needed below.

[Jovan Gerbscheid]

Here's a fix for this particular case: #13628

[Yury G. Kudryashov]

Delegated