Proving membership of a set literal in Lean 4

Stream: new members

[gldanoob]

I encountered something like

⊢ Char.ofNat 98 ∈ {Char.ofNat 97, Char.ofNat 98, Char.ofNat 99}

in the middle of a proof. I've tried constructor and unfold insert without luck. How should I proceed, and where can I find information about the relevant theorems?

[Kyle Miller]

Have you tried simp?

[Kyle Miller]

In any case, the way set membership with a set literal works is that it's ultimately an Or of Eqs, so you should be able to do right; left; rfl.

[Ruben Van de Velde]

rw? should probably come up with something too