Zulip Chat Archive

Stream: new members

Topic: How to check element is in set

Andrea Nardi (Nov 06 2022 at 21:09):

Given the following code

inductive Test : Type
| T1 | T2

example : Test.T1  { t: Test | t = Test.T1 } := begin

how do I prove this in tactic mode?

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

Thank you in advance

David Renshaw (Nov 06 2022 at 21:10):

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

David Renshaw (Nov 06 2022 at 21:11):

e.g. simp

Kyle Miller (Nov 06 2022 at 21:11):

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 (Nov 06 2022 at 21:13):

(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 (Nov 06 2022 at 22:12):

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

Yakov Pechersky (Nov 06 2022 at 22:38):


Last updated: Dec 20 2023 at 11:08 UTC