!4#3622 Analysis.Convex.Jensen

Stream: mathlib4

[Jeremy Tan]

I have the following universe error at L129:

invalid occurrence of universe level 'u_4' at 'ConvexOn.exists_ge_of_mem_convexHull', it does not occur at the declaration type, nor it is explicit universe level provided by the user, occurring at expression
  Exists.casesOn.{u_4 + 2}
    (Eq.mp.{0}
      (Eq.ndrec.{0, u_2 + 1} (Eq.refl.{1} (Membership.mem.{u_2, u_2} x (↑(convexHull.{u_1, u_2} 𝕜).toOrderHom s)))
        (_root_.convexHull_eq.{u_1, u_2, u_4} s))
      hx)
    fun α h =>
    Exists.casesOn.{u_4 + 1} h fun t h =>
      Exists.casesOn.{max (u_4 + 1) (u_1 + 1)} h fun w h =>
        Exists.casesOn.{max (u_4 + 1) (u_2 + 1)} h fun p h =>
          Exists.casesOn.{0} h fun hw₀ h =>
            Exists.casesOn.{0} h fun hw₁ h =>
              Exists.casesOn.{0} h fun hp h =>
                Eq.ndrec.{0, u_2 + 1}
                  (Exists.casesOn.{u_4 + 1}
                    (exists_ge_of_centerMass.{u_4, u_3, u_2, u_1} hf hw₀
                      (Eq.rec.{0, u_1 + 1} zero_lt_one.{u_1} (Eq.symm.{u_1 + 1} hw₁)) fun i hi =>
                      subset_convexHull.{u_1, u_2} 𝕜 s (hp i hi))
                    fun i h => And.casesOn.{0} h fun hit Hi => Exists.intro.{u_2 + 1} (p i) (And.intro (hp i hit) Hi))
                  h
at declaration body
  fun {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [LinearOrderedAddCommGroup β]
      [Module 𝕜 E] [Module 𝕜 β] [OrderedSMul 𝕜 β] {s : Set E} {f : E → β}
      (hf : ConvexOn 𝕜 (↑(convexHull 𝕜).toOrderHom s) f) {x : E} (hx : x ∈ ↑(convexHull 𝕜).toOrderHom s) =>
    Exists.casesOn (Eq.mp (_root_.convexHull_eq s ▸ Eq.refl (x ∈ ↑(convexHull 𝕜).toOrderHom s)) hx)
      fun (α : Type u_4)
        (h :
          ∃ (t : Finset α),
            ∃ (w : α → 𝕜),
              ∃ (z : α → E),
                ∃ (x_1 : ∀ (i : α), i ∈ t → 0 ≤ w i),
                  ∃ (x_2 : (Finset.sum t fun (i : α) => w i) = 1),
                    ∃ (x_3 : ∀ (i : α), i ∈ t → z i ∈ s), centerMass t w z = x) =>
      Exists.casesOn h
        fun (t : Finset α)
          (h :
            ∃ (w : α → 𝕜),
              ∃ (z : α → E),
                ∃ (x_1 : ∀ (i : α), i ∈ t → 0 ≤ w i),
                  ∃ (x_2 : (Finset.sum t fun (i : α) => w i) = 1),
                    ∃ (x_3 : ∀ (i : α), i ∈ t → z i ∈ s), centerMass t w z = x) =>
        Exists.casesOn h
          fun (w : α → 𝕜)
            (h :
              ∃ (z : α → E),
                ∃ (x_1 : ∀ (i : α), i ∈ t → 0 ≤ w i),
                  ∃ (x_2 : (Finset.sum t fun (i : α) => w i) = 1),
                    ∃ (x_3 : ∀ (i : α), i ∈ t → z i ∈ s), centerMass t w z = x) =>
          Exists.casesOn h
            fun (p : α → E)
              (h :
                ∃ (x_1 : ∀ (i : α), i ∈ t → 0 ≤ w i),
                  ∃ (x_2 : (Finset.sum t fun (i : α) => w i) = 1),
                    ∃ (x_3 : ∀ (i : α), i ∈ t → p i ∈ s), centerMass t w p = x) =>
            Exists.casesOn h
              fun (hw₀ : ∀ (i : α), i ∈ t → 0 ≤ w i)
                (h :
                  ∃ (x_1 : (Finset.sum t fun (i : α) => w i) = 1),
                    ∃ (x_2 : ∀ (i : α), i ∈ t → p i ∈ s), centerMass t w p = x) =>
              Exists.casesOn h
                fun (hw₁ : (Finset.sum t fun (i : α) => w i) = 1)
                  (h : ∃ (x_1 : ∀ (i : α), i ∈ t → p i ∈ s), centerMass t w p = x) =>
                Exists.casesOn h fun (hp : ∀ (i : α), i ∈ t → p i ∈ s) (h : centerMass t w p = x) =>
                  h ▸
                    Exists.casesOn
                      (exists_ge_of_centerMass hf hw₀ (Eq.symm hw₁ ▸ zero_lt_one) fun (i : α) (hi : i ∈ t) =>
                        subset_convexHull 𝕜 s (hp i hi))
                      fun (i : α) (h : i ∈ t ∧ f (centerMass t (fun (i : α) => w i) fun (i : α) => p i) ≤ f (p i)) =>
                      And.casesOn h
                        fun (hit : i ∈ t) (Hi : f (centerMass t (fun (i : α) => w i) fun (i : α) => p i) ≤ f (p i)) =>
                        Exists.intro (p i) { left := hp i hit, right := Hi }

How do I fix it?

[Jeremy Tan]

The file doesn't have any explicit universe declarations at all, which to me feels weird

[Moritz Doll]

for convexHull_eq you have to give an explicit universe level for the type in the existential quantifier, see my fix for Analysis.Convex.Combination

[Jeremy Tan]

Right, that worked