Simple Uniform Probability

Stream: new members

[Mukesh Tiwari]

Hi Everyone, I am trying to model a simple proof, but I am getting "invalid match/convoy expression, expected type is not known" https://gist.github.com/mukeshtiwari/f5692ca8bacac1c2bcb44386194a0e2a

[Reid Barton]

I don't know how to account for that specific error message, but surely uniform should be mentioned somewhere in the statement.
But an easier way to write the statement is something like finset.univ.sum uniform = 1.