Universes issue in mathlib#1464

Stream: mathlib4

[Arien Malec]

Can someone who groks universe issue deeply have a look at mathlib4#1464?

I've compared mathlib and the mathport version here and I'm not sure I understand what's up. I assume this is due to the variable declarations and maybe the differences between Type* and Type _? I've tried to look for simple fixes....

[Heather Macbeth]

(wrong link)

[Arien Malec]

fixed -- thanks!