## Stream: general

### Topic: iff eq cancel left

#### 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


#### Kevin Buzzard (Aug 05 2019 at 08:14):

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

#### Chris Hughes (Aug 05 2019 at 11:14):

rw h does it.

#### Kevin Buzzard (Aug 05 2019 at 11:21):

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

#### Kevin Buzzard (Aug 05 2019 at 11:22):

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

#### Chris Hughes (Aug 05 2019 at 11:32):

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

#### Johan Commelin (Aug 05 2019 at 11:35):

Because you might want to apply it

#### Johan Commelin (Aug 05 2019 at 11:36):

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

#### Chris Hughes (Aug 05 2019 at 11:37):

I would prefer suffices in that situation. More readable.

#### Kevin Buzzard (Aug 05 2019 at 11:39):

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

#### Johan Commelin (Aug 05 2019 at 11:39):

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

#### 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

#### Reid Barton (Aug 05 2019 at 11:41):

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

#### 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