1
$\begingroup$

Given this code,

inductive Test : Type
| T1 | T2

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

How do I prove that Test.T1 ∈ { t: Test | t = Test.T1 } (which trivially seems to be the case)?
I tried the intro tactic but it did not work.

$\endgroup$
1
  • $\begingroup$ What you need to know is how things are defined under the hood. By definition, x \in {a : X | P a} means P x, so your goal is definitionally equal to Test.T1 = Test.T1. $\endgroup$ Nov 6, 2022 at 21:56

1 Answer 1

2
$\begingroup$

rfl should do the trick:

inductive Test : Type
| T1 | T2

example : Test.T1 ∈ { t: Test | t = Test.T1 } := rfl
$\endgroup$
2
  • $\begingroup$ This seems to work. Is there a way of solving it in tactics mode? refl does not seem to work. $\endgroup$ Nov 6, 2022 at 20:48
  • 1
    $\begingroup$ @AndreaNardi The tactics simp and exact rfl and split seem to work. $\endgroup$
    – Jason Rute
    Nov 6, 2022 at 21:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.