unnecessary universe variable?

Stream: mathlib4

[Edward van de Meent]

the lemma Cardinal.mk_compl_eq_mk_compl_finite_same currently parametrises over two universe variables, one of which is only used during the proof, and does not occur in the statement.

In order to make this declaration compatible for branch#byAsSorry , i need to either somehow make clear that this universe variable is used/neccessary, or remove uses of the variable from the proof.

I have managed to find a way to do the second, but as I'm not very experienced when it comes to using universe variables, i'd like to know if this is an option that is desirable.

[Joël Riou]

If a statement needs only one universe parameter, we should not introduce unnecessary universes in the proof. In this case, replacing max u v by u in the proof removes the dependency on v.

[Edward van de Meent]

indeed, that was the fix i found too. do i understand correctly that removing the extra variable doesn't result in any usability issues?