Zulip Chat Archive

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