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