Wrong universes

Stream: mathlib4

[Antoine Chambert-Loir]

I was trying to help porting !4#4929
Lean can't find an instance it should find, and doing explicitly as typed in by @Yury G. Kudryashov , I get wrong universes (around line 1380) : (max (max (max (max uE' uF) uG) uP) uE) instead of max (max (max uF uG uP) uE' uG uP) uE

[Antoine Chambert-Loir]

(Anyway, I don't have the right to push the small successful modification I could make)

[Mario Carneiro]

I doubt that has any effect

[Mario Carneiro]

it might not be normalized but it should not affect defeq queries etc

[Antoine Chambert-Loir]

You're right, there is a subtle difference that may explain why Lean4 isn't happy, I didn't read the error message carefully enough…

The full error message is

type mismatch
  hasOpNorm
has type
  Norm
    (@ContinuousLinearMap 𝕜 𝕜 DivisionSemiring.toSemiring DivisionSemiring.toSemiring (RingHom.id 𝕜) E
      UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid ((P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F)
      UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid NormedSpace.toModule
      NormedSpace.toModule) : Type (max (max (max (max uE' uF) uG) uP) uE)
but is expected to have type
  Norm
    (@ContinuousLinearMap 𝕜 𝕜 DivisionSemiring.toSemiring DivisionSemiring.toSemiring (RingHom.id 𝕜) E
      UniformSpace.toTopologicalSpace AddCommGroup.toAddCommMonoid ((P × G →L[𝕜] E') →L[𝕜] P × G →L[𝕜] F)
      topologicalSpace addCommMonoid NormedSpace.toModule module) : Type (max (max (max uF uG uP) uE' uG uP) uE)

(Starting with Norm, the first three lines starting are identical, but there is a difference in the last one.)

[Mario Carneiro]

I assume module is a local variable?

[Mario Carneiro]

you should look at the isDefEq trace, there is a lot of irrelevant difference here and implicit arguments

[Kevin Buzzard]

Does topologicalSpace (a human-made instance, presumably, in the second half of the error) definitely match up with what it's supposed to match up with in the first half of the error?

[Scott Morrison]

Antoine Chambert-Loir said:

(Anyway, I don't have the right to push the small successful modification I could make)

@Antoine Chambert-Loir, what is your github username?

[Ruben Van de Velde]

I can't see where module comes from in the PR; have you already made changes? If you introduced it, check if you need to use letI

[Yaël Dillies]

@Scott Morrison, it's AntoineChambert-Loir.

[Scott Morrison]

Invite to mathlib4 sent!

[Yury G. Kudryashov]

@Antoine Chambert-Loir Did you fix one of the proofs? If yes, which one?

[Yury G. Kudryashov]

Generally, it's better to work on PRs that have help-wanted label.

[Yury G. Kudryashov]

I'm trying to fix HasCompactSupport.hasFDerivAt_convolution_right right now.

[Antoine Chambert-Loir]

Scott Morrison said:

Antoine Chambert-Loir said:

(Anyway, I don't have the right to push the small successful modification I could make)

Antoine Chambert-Loir, what is your github username?

AntoineChambert-Loir

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

Antoine Chambert-Loir Did you fix one of the proofs? If yes, which one?

HasCompactSupport.hasFDerivAt_convolution_right

[Yury G. Kudryashov]

@Antoine Chambert-Loir Push the fix, please.

[Yury G. Kudryashov]

I see that you've already pushed.

[Antoine Chambert-Loir]

I think I just did! I'll check as soon as i I can switch my computer on!

⁣--
Université Paris Cité
Institut de mathématiques de Jussieu Paris Rive Gauche
Bâtiment Sophie Germain, 8 place Aurélie Nemours, 75205 Paris cedex 13

Envoyé depuis mon téléphone portable, pardonnez mon éventuelle brièveté​

⁣--
Université Paris Cité
Institut de mathématiques de Jussieu Paris Rive Gauche
Bâtiment Sophie Germain, 8 place Aurélie Nemours, 75205 Paris cedex 13

Envoyé depuis mon téléphone portable, pardonnez mon éventuelle brièveté​

[Yury G. Kudryashov]

Indeed, I wrote before looking at github.