Zulip Chat Archive

Stream: general

Topic: iff eq cancel left


view this post on Zulip Johan Commelin (Aug 05 2019 at 07:37):

Is it true that this is not in the library?

lemma iff.eq_cancel_left {α : Type*} {a b c : α} (h : b = c) :
  (a = b  a = c) := by library_search -- fails

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 08:14):

Does simp [h] do it? If so you could look and see how

view this post on Zulip Chris Hughes (Aug 05 2019 at 11:14):

rw h does it.

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 11:21):

yeah but that doesn't tell us if it's in the library :-)

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 11:22):

It looks like it should be in equiv, it follows from symm and trans

view this post on Zulip Chris Hughes (Aug 05 2019 at 11:32):

Why would it be in the library when it's one rw?

view this post on Zulip Johan Commelin (Aug 05 2019 at 11:35):

Because you might want to apply it

view this post on Zulip Johan Commelin (Aug 05 2019 at 11:36):

If I have complicated_foo = 1 ↔ complicated_bar = 1...

view this post on Zulip Chris Hughes (Aug 05 2019 at 11:37):

I would prefer suffices in that situation. More readable.

view this post on Zulip Kevin Buzzard (Aug 05 2019 at 11:39):

This from the man who thinks le is more readable than subset ;-)

view this post on Zulip Johan Commelin (Aug 05 2019 at 11:39):

Sometimes that would mean adding 15 type ascriptions while telling Lean what suffices.

view this post on Zulip Johan Commelin (Aug 05 2019 at 11:40):

And complicated_foo = 1 suddenly becomes (very : complicated) (why : am_I_writing_this) (horrible : long_goal) foo = 1

view this post on Zulip Reid Barton (Aug 05 2019 at 11:41):

It would be nice if you could use congr to take care of the iff

view this post on Zulip Chris Hughes (Aug 05 2019 at 11:42):

How about apply iff_of_eq (congr_arg _ h)


Last updated: May 13 2021 at 21:12 UTC