Change coe_singleton type to explicitly convert Set -> _root_.Set

[Shaunticlair]

Currently, the original version seems to be functionally stating

({x}: _root_.Set Object) = ({x}: _root_.Set Object)

Which doesn't relate to coercion to SetTheory.Set. Here, I've made the initial casting to SetTheory.Set on the lefthand side explicit, so the thoerem actually demonstrates that coercing singleton ({x} : SetTheory.Set) to _root_.Set is the same as if you initially built the singleton in _root_.Set.

[Shaunticlair]

Notably, SetTheory.Set.coe_union has a similar issue: somehow (I don't know Lean well enough to know how/why), it immediately manages to break down inst_coe_set.coe (X ∪ Y) into inst_coe_set.coe (X) ∪ inst_coe_set.coe (Y). In other words, coercing ∪ from a _root_.Set into a SetTheory.Set operation, instead of directly coercing the set X ∪ Y.

Meaning, we get

{x | x ∈ X} ∪ {x | x ∈ Y} = {x | x ∈ X} ∪ {x | x ∈ Y}

Instead of, presumably the intended version,

{x | x ∈ X ∪ Y} = {x | x ∈ X} ∪ {x | x ∈ Y}

I didn't add this one to the push request because it seems possible that this is actually the intended demonstration, since it's still showing a _root_.Set to SetTheory.Set coercion.

[Shaunticlair]

coe_pair, coe_intersection, and coe_diff seem to also have this sort of behavior. Leaving them unmodified while waiting for confirmation.

[teorth]

You're right; for instance, in the left-hand side of SetTheory.Set.coe_union, (X ∪ Y : _root_.Set Object) should be (X ∪ Y : Set). If you can change this (and make similar changes in the other theorems you mentioned) that would be great.