## Stream: new members

### Topic: Set difference

#### Dan Stanescu (Aug 22 2020 at 20:16):

Can someone please point me to the simplest way to get false from j ∈ finset.range (n + 1) \ {j}?

#### Kyle Miller (Aug 22 2020 at 20:19):

This apparently worked:

example {j n : ℕ} : j ∈ finset.range (n + 1) \ {j} → false :=
begin
tidy,
end


You can use tidy? to figure out what it saw.

#### Kyle Miller (Aug 22 2020 at 20:19):

Apparently it went through this, which you probably can simplify further:

simp only [forall_prop_of_false, eq_self_iff_true, not_true, finset.mem_sdiff, not_false_iff, finset.mem_singleton, and_false]


#### Dan Stanescu (Aug 22 2020 at 20:20):

Thank you! I didn't have tidy on my radar yet.

#### Kyle Miller (Aug 22 2020 at 20:20):

simp would have worked, too. I just pulled out the big guns first.

#### Dan Stanescu (Aug 22 2020 at 20:21):

No, simp didn't work for me.

#### Dan Stanescu (Aug 22 2020 at 20:21):

Don't understand why.

#### Kyle Miller (Aug 22 2020 at 20:21):

It worked for me, that's strange.

#### Kyle Miller (Aug 22 2020 at 20:22):

So this doesn't work for you?

example {j n : ℕ} (h : j ∈ finset.range (n + 1) \ {j}) : false :=
begin
simp at h,
end


#### Dan Stanescu (Aug 22 2020 at 20:23):

Oh wait, I don't have the latest mathlib version, although I'm using 3.18.4. I doubt, but could this be it?

#### Kyle Miller (Aug 22 2020 at 20:23):

A shorter proof:

example {j n : ℕ} (h : j ∈ finset.range (n + 1) \ {j}) : false :=
begin
rw finset.mem_sdiff at h,
rw finset.mem_singleton at h,
cc, -- this sees ¬j = j and proves false
end


#### Kyle Miller (Aug 22 2020 at 20:24):

I'm using 3.18.4, too.

#### Kyle Miller (Aug 22 2020 at 20:24):

I assume you have import tactic at the top of your file?

#### Kyle Miller (Aug 22 2020 at 20:26):

Oh, cc was overkill:

example {j n : ℕ} (h : j ∈ finset.range (n + 1) \ {j}) : false :=
begin
rw finset.mem_sdiff at h,
rw finset.mem_singleton at h,
exact h.2 rfl,
end


#### Dan Stanescu (Aug 22 2020 at 20:26):

I do. Actually it was probably my fault. I had that as a hypothesis H and should have done simp at H. Instead I tried simp directly, thinking that it would produce the false goal.

#### Dan Stanescu (Aug 22 2020 at 20:27):

Thanks @Kyle Miller !

Last updated: Dec 20 2023 at 11:08 UTC