Subset of subset

Stream: new members

[Thomas Browning]

If B : set C, and A : set B, how do you get (a version of) A in set C?

[Adam Topaz]

Try something like subtype.val '' A

[Yury G. Kudryashov]

We recently decided that the simp-normal form is coe, not subtype.val.

[Yury G. Kudryashov]

So, (coe '' A : set C)

[Eric Wieser]

By this, you mean that we should never type subtype.val or x.val in a proof or lemma?

[Reid Barton]

No, this is much too strong. Just don't use it in the statement of a simp lemma, especially on the left-hand side. You might find it useful to avoid using it in other places too.

[Kevin Buzzard]

@Eric Wieser do you know about simp normal form? The idea is that if you want to get simp working for you, you should know what the form is which the lemmas are trying to normalise towards. The idea is that when your goal is in the "right" form when you can just apply standard theorems, but all the theorems need to be stated in the "right" form too. So you need to make some design decision about what all your lemmas will look like, and then try and stick to this notation in the middle of proofs.