interesting problem with Mathlib minimization

Stream: mathlib4

[Kim Morrison]

I've recently written https://github.com/kim-em/lean-minimizer, a general purpose Lean test case reducer (i.e. takes a file demonstrating a bug, and produces a smaller/simpler file, with fewer imports, demonstrating the same bug). (Usage reports / bug reports very very welcome!) If you're minimizing a file that imports Mathlib, it's convenient to use https://github.com/kim-em/mathilb-minimizer, which additionally requires Mathlib.

[Kim Morrison]

I've just encountered an interesting situation, which I would be happy to have help with. This is a case where I have a file with an import, but inlining that import causes compilation to fail.

[Kim Morrison]

(For context, I'm trying to minimize a proof from Mathlib/Analysis/ODE/PicardLindelof.lean that seems to sporadically generate a PANIC in grind.)

[Kim Morrison]

Here's https://gist.github.com/kim-em/6c6f201a8e8d9592b3b7da44ad9053c8 which is a partial minimization of that theorem. It compiles fine. After inlining the import Mathlib.Analysis.Normed.Module.Multilinear.Basic (i.e. just adding section Mathlib.Analysis.Normed.Module.Multilinear.Basic and end Mathlib.Analysis.Normed.Module.Multilinear.Basic at the top of the file, and moving the contents of Mathlib.Analysis.Normed.Module.Multilinear.Basic into that section, and moving the import statements back to the top of the file), the resulting file fails to compile (see live.lean-lang.org) with an error

failed to synthesize instance of type class
  Norm (ContinuousMultilinearMap 𝕜 E 𝕜 →L[𝕜] G →L[𝕜] ContinuousMultilinearMap 𝕜 E G)

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

at

lemma norm_smulRightL_le : ‖smulRightL 𝕜 E G‖ ≤ 1 :=
  LinearMap.mkContinuous₂_norm_le _ zero_le_one _

[Kim Morrison]

I'm a bit stumped how this can work before inlining but not afterwards. Assistance very much appreciated. Being able to reliably minimize test cases will really help the FRO help Mathlib!

[Andrew Yang]

Mathlib has maxSynthPendingDepth set to 3 by default. It works if you add set_option maxSynthPendingDepth 3 in before the lemma.

[Kim Morrison]

Nice catch! I will add this setting to the mathlib-minimizer lakefile.