## Stream: new members

### Topic: How to unfold \in

#### Jason Orendorff (Jun 15 2020 at 13:39):

I'm trying to prove this:

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
(hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := sorry


I don't know which tactic to use to break open the ∈ propositions.

#### Scott Morrison (Jun 15 2020 at 13:41):

dsimp [(∈)]

#### Scott Morrison (Jun 15 2020 at 13:41):

but almost certainly this isn't actually what you want to do

#### Jason Orendorff (Jun 15 2020 at 13:43):

Thanks for both answers

#### Jalex Stark (Jun 15 2020 at 14:08):

the theorem is called list.mem_filter and it is a simp lemma. I found it like this:

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
(hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := begin
squeeze_simp at hmem,
end


#### ROCKY KAMEN-RUBIO (Jun 15 2020 at 19:02):

set.mem_set_of_eq can also be useful

#### Jason Orendorff (Jun 15 2020 at 19:12):

Thanks. The output I get from this

import tactic.squeeze
import tactic.basic

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
(hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := begin
squeeze_simp at hmem,
end


is "simplify tactic failed to simplify". Do I need something else?

#### Jalex Stark (Jun 15 2020 at 19:14):

sorry for not including my imports. You'll need whatever file list.mem_filter is defined in, since it's only added to simp once it's defined

#### Jalex Stark (Jun 15 2020 at 19:14):

which should be data.list.basic

#### Jalex Stark (Jun 15 2020 at 19:15):

so this works:

import tactic

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
(hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := begin
squeeze_simp at hmem,
end


#### Jalex Stark (Jun 15 2020 at 19:16):

and so does this

import tactic.basic
import data.list.basic

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
(hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := begin
squeeze_simp at hmem,
end


#### Jalex Stark (Jun 15 2020 at 19:17):

I personally always work with import tactic, rather than importing only the tactics I need; I think there's no downside to this unless you're working on contributions to mathlib, where you have to be more aware of the dependency graph

#### Jason Orendorff (Jun 15 2020 at 19:17):

ok. thanks again! is there somewhere i can read about this?

read about what?

#### Jalex Stark (Jun 15 2020 at 19:19):

the docs page for data.list.basic? https://leanprover-community.github.io/mathlib_docs/data/list/basic.html

#### Jason Orendorff (Jun 15 2020 at 19:21):

i meant, what should I have read, to know that import tactic exists!

#### Jason Orendorff (Jun 15 2020 at 19:22):

the language reference doesn't mention import

#### Jason Orendorff (Jun 15 2020 at 19:22):

—that I could see, I didn't read the whole thing

#### Kevin Buzzard (Jun 15 2020 at 19:27):

This is one of the things you pick up on the chat :-)

#### Jalex Stark (Jun 15 2020 at 19:34):

did you do any tutorials? there should be lots of files in the tutorials that start with import tactic?

#### Kevin Buzzard (Jun 15 2020 at 19:37):

Whether or not import tactic is useful to you is very much subject-dependent. There are people here who are writing little implementations of theories who don't need any tactics at all other than those in core; there are people who actively don't want to import mathlib; there are undergraduate mathematicians who are just completely lost without ring and linarith and are encouraged by me to switch on classical logic and import all tactics on line 1.

#### Jason Orendorff (Jun 15 2020 at 21:58):

So far I've just read _Theorem Proving In Lean_, worked its examples, and done the Natural Numbers Game, dipped into the reference manual, and noodled around in lean/library/init a bit

#### Kevin Buzzard (Jun 15 2020 at 21:59):

Well the next step is to think of some formalisation project and to get going :-) I did 50 1st year maths undergraduate level questions next (which happened to be the 50 questions I was setting my own undergraduates), got stuck 40 times and asked here ;-)

#### Jalex Stark (Jun 15 2020 at 22:00):

if you want more reading, Mathematics in lean #mil probably has things interesting to you

#### Jalex Stark (Jun 15 2020 at 22:00):

reading the archives on zulip is also pretty effective, you can pick up "folklore
knowledge" that hasn't made its way into polished tutorials

#### Kevin Buzzard (Jun 15 2020 at 22:01):

Given that Patrick, Jeremy and I are all rapidly approaching the end of term/semester, hopefully MIL will have even more interesting things soon.

#### Jason Orendorff (Jun 15 2020 at 22:07):

yeah, MIL is next for me, but leanprover get tutorials also beckons

#### Jalex Stark (Jun 15 2020 at 22:11):

you probably mean leanproject get tutorials

#### Jason Orendorff (Jun 16 2020 at 14:50):

yes

Last updated: May 15 2021 at 23:13 UTC