## Stream: Is there code for X?

### Topic: set.univ is \top

#### Eric Wieser (Nov 10 2020 at 13:38):

I ended up stuck with this as a subgoal, which was quite annoying:

example  (A : Type*) (a : A) : a ∈ (⊤ : set A) := sorry


The solution is set.mem_univ a, but neither simp nor library_search were able to find it. Should there be a lemma for this?

#### Anne Baanen (Nov 10 2020 at 13:40):

I'd like to see a @[simp] lemma : (⊤ : set A) = univ.

#### Eric Wieser (Nov 10 2020 at 13:53):

Looks like it was just forgotten, docs#set.bot_eq_empty is there

I'll make a PR

#4963

#### Kevin Buzzard (Nov 10 2020 at 14:15):

I guess the "canonical form" for (⊤ : set A) is univ in the library. simp is usually something which proves equalities and <->s rather than random simple facts, I guess.

#### Eric Wieser (Nov 10 2020 at 14:24):

My reading was that simp has a second job, which is to turn things into canonical forms

#### Eric Wieser (Nov 10 2020 at 14:24):

(eg how we have docs#monoid_hom.to_fun_eq_coe)

#### Kevin Buzzard (Nov 10 2020 at 14:39):

Yeah you're dead right, and Anne's simp lemma is doing exactly that. I guess I'm saying that Anne's approach is the correct one for simp`, rather than adding your original subgoal as a simp lemma.

Last updated: May 07 2021 at 21:10 UTC