Help me with a universe level problem

Stream: new members

[nemo]

I am trying to prove the following theorem

lemma pres_assoc (ι₁ : Sort u₁) [CoeSort ι₁ (Sort v₁)]
  (ι₂ : Sort u₂) [CoeSort ι₂ (Sort v₂)]
  (α : Type w) :
  (
    Pres ((Pres ι₁ ι₂) ) α
    : Sort (max 1 u₁ v₁ v₂ (imax v₁ u₂) (w + 1))
  )
  =
  (
    Pres ι₁ (Pres ι₂ α)
    : Sort (max 1 u₁ v₁ v₂ u₂ (w + 1))
  )

but my computer is throwing a type mismatch exception

type mismatch
  Pres ι₁ (Pres ι₂ α)
has type
  Sort (max u₁ 1 v₁ (max 1 u₂) v₂ (w + 1)) : Type (max u₁ 1 v₁ (max 1 u₂) v₂ (w + 1))
but is expected to have type
  Sort
    (max (max (max 1 u₁) (imax v₁ u₂)) 1 (max (max 1 v₁) v₂)
        (w + 1)) : Type (max (max (max 1 u₁) (imax v₁ u₂)) 1 (max (max 1 v₁) v₂) (w + 1))

I can see that the two levels are equal by casing u\2 with 0 and succ, but it seems lean4 can't see that. So what can I do?

[nemo]

I have just realized that by my definition, the two sorts are not identical, but only equivalent. But I think it's still an unpleasant problem that lean dosen't know they are in the same universe

[Aaron Liu]

Yeah unfortunately it doesn't case (but it totally could)