set.univ is \top

Stream: Is there code for X?

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

I'll make a PR

[Eric Wieser]

#4963

[Kevin Buzzard]

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]

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

[Eric Wieser]

(eg how we have docs#monoid_hom.to_fun_eq_coe)

[Kevin Buzzard]

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.