subset from finset declaration

Stream: new members

[Manuel Candales]

I am defining a finset like: {e ∈ finset.range n | 2 ∣ e }, and I want to show that it is a subset of finset.range

import data.finset

example (n : ℕ) (M : finset ℕ := {e ∈ finset.range n | 2 ∣ e }) : M ⊆ finset.range n :=
begin
  sorry,
end

I tried simp, dsimp, hint, library_search, suggest. Nothing worked.
I tried defining M using finset.filter as follows, to then apply finset.filter_subset.

import data.finset

example (n : ℕ) (p : ℕ → Prop := (λ e, 2 ∣ e)) (M : finset ℕ := finset.filter p (finset.range n)) :
  M ⊆ finset.range n :=
begin
  sorry,
end

But this is giving me an error, asking for ⊢ decidable_pred p.
Could someone please point me in the right direction?

[Yakov Pechersky]

example (n : ℕ) (p : ℕ → Prop) (hp : p = λ e, 2 ∣ e) [decidable_pred p] (M : finset ℕ)
  (hM : M = finset.filter p (finset.range n)) :
  M ⊆ finset.range n :=
begin
  rw hM,
  exact finset.filter_subset p _,
end

[Yakov Pechersky]

Or write open_locale classical

open_locale classical

example (n : ℕ) (p : ℕ → Prop) (hp : p = λ e, 2 ∣ e) (M : finset ℕ)
  (hM : M = finset.filter p (finset.range n)) :
  M ⊆ finset.range n :=
begin
  rw hM,
  exact finset.filter_subset p _,
end

[Yakov Pechersky]

example (n : ℕ) (M : finset ℕ)
  (hM : M = finset.filter (λ e, 2 ∣ e) (finset.range n)) :
  M ⊆ finset.range n :=
begin
  rw hM,
  exact finset.filter_subset _ _,
end

[Yakov Pechersky]

When you say what p is equal to in a separate hypothesis, that doesn't let the finset.filter in the body of the lemma/example statement know that it is decidable.

[Manuel Candales]

Thank you! open_locale classical helped!