Proving that all elements of fin set are in another fin set

Stream: general

[Daniel Garcia]

I am trying to figure out a small example of how to show that all elements in one finite set are in another, but I am having some issues trying to show this. Thank you in advance!

import Mathlib.Tactic
example: ({1, 2}: Finset ℤ)  ⊆ {1, 2, 3} := by
intro x hx
cases hx
simp
sorry -- How to deal with this hypothesis? a✝: List.Mem x [2]

[Floris van Doorn]

Note that decide and simp can prove the whole goal for you.

[Daniel Garcia]

Thank you so much! That worked for me!

[Floris van Doorn]

On the actual place of your sorry, seems that Mathlib is missing the lemma

@[simp] lemma List.mem_def {α : Type*} {l : List α} {x : α} :
  List.Mem x l ↔ x ∈ l := .rfl

which would rewrite your hypothesis in a form that simp can deal with further.