Equality is not provable. Indeed, it is consistent that univ.{u u+1} < #(Type u) at every level u.
Recall that the universe level operations that Lean allows are quite limited. (See Mario Carneiro, The Type Theory of Lean, for all the details.) The level terms are built from universe variables using only: 0, ∙+1, max(∙,∙) and imax(∙,∙). Because these operations are so limited, it is possible to give nontrivial self-interpretations of Lean's type theory in itself.
Let f be any strictly increasing function from levels to levels such that f(0) = 0. Consider the interpretation of Lean in itself where Sort u is reinterpreted as Sort f(u). Thus the new universe levels are only those in the range of f and the successor operation ∙+1 is reinterpreted so that f(u)+1 is now f(u+1). Everything in Lean's type theory works as-is with just a few exceptions. For example, Sort u : Sort u+1 doesn't work on-the-nose; similarly with some inductive types. There's a couple of different ways to patch this, the details are immaterial. (If Lean's type theory were cumulative there would essentially be nothing to fix.)
Now consider this self-interpretation where, for example, f(0)=0, f(1) = 1, ..., f(42) = 42 but f(43) = 44, f(44) = 45, etc. In this interpretation, Type 41 (= Sort 42) is unchanged but Type 42 is now the old Type 43. It follows that univ.{41 42} (which is basically the old univ.{41 43}) is strictly smaller than #(Type 42) (which is the old #(Type 43)). This is because the original univ.{42 43} and #(Type 42) still exists in between these two cardinals, even though they have lost their particular meaning in the new interpretation.
univ.{u u+1} = # (Type u)is independent of Lean. Almost anything that talks about equality of types is independent of Lean. For example, I wouldn't be surprised if# {A : Type u // is_empty A } > univ.{u u+1}is consistent with Lean. $\endgroup$