How to check element is in set

Stream: new members

[Andrea Nardi]

Given the following code

inductive Test : Type
| T1 | T2

example : Test.T1 ∈ { t: Test | t = Test.T1 } := begin
  sorry
end

how do I prove this in tactic mode?

Also, how do I make a singleton set in Lean?

Thank you in advance

[David Renshaw]

The hint tactic shows that there are a bunch of different tactics which close that goal.

[David Renshaw]

e.g. simp

[Kyle Miller]

There's a term-mode proof at https://proofassistants.stackexchange.com/questions/1825/how-do-i-prove-that-an-element-is-a-within-a-set-in-lean

You mention refl doesn't work, but you can do exact rfl as a workaround

[Kyle Miller]

(refl applies a reflexivity lemma based on what it sees, and it can't see it's proving an eq in this case)

[Kevin Buzzard]

you can change Test.T1 = Test.T1 to make definitional changes to your goal.

[Yakov Pechersky]

docs#set.mem_set_of