Sets in Mathlib4

Stream: new members

[Jonathan Whitehead]

Hey all,

I'm just getting started and I keep getting a type error when I'm just trying to define something as simple as a subset. I tried to do it similar to the lean3 tutorial but this is what I get:

image.png

Can someone explain to me how to fix this? Moreover, can someone explain to me the process of solving type errors like this in the future. For example, it says "type expected, got ... (set U : ?m.0 PUnit)". I don't know how to interpret this error. I don't know what the ?m.0 PUnit means or how to resolve something like this.

[Heather Macbeth]

Capital s! Set

[Jonathan Whitehead]

Thanks!