Error in Set Theory Game

Stream: Lean for teaching

[Gridiron Player]

image.png

Does anybody know why this would give me a type error?

[Chris Henson]

For sets, membership should have types Membership α (Set α). The error is because you're ending up with something like Membership (Set α) (Set α), where α is Set U. It doesn't make sense for the elements and the set to be the same type.

[Jon Eugster]

So in plain text F ∈ F ∪ G looks wrong and you probably want F ⊆ F ∪ G, don't you? Or use something else than F to be an element of your union? Further, your have-syntax seems wrong with that comma in there

[Dan Velleman]

F and G have type Set (Set U), so an element of F ∪ G has to have type Set U. That means you can only apply h to something of type Set U. Since F has type Set (Set U), it doesn't make sense to apply h to F. That's why Lean is complaining.

If you had something in your context of type Set U -- in particular, something that is an element of F ∪ G -- then it would make sense to apply h to it. But you don't have anything like that in your context, so it seems unlikely that applying h is a good next step. I would look more closely at the goal. Have you thought about what the goal means, and what you would have to do to prove it?

By the way, there is another mistake in your have step: ∀ t ∈ F ∪ G, x ∈ t is shorthand for ∀ (t : Set U), t ∈ F ∪ G → x ∈ t. So if you apply h to some object w of type Set U, then the result will be w ∈ F ∪ G → x ∈ w, not w ∈ F ∪ G, x ∈ w. In fact, w ∈ F ∪ G, x ∈ w doesn't make sense -- if you want to combine two statements to make a new statement, you have to connect them with a logical connective, not a comma.

[Gridiron Player]

Thanks guys, I figured that one out!