iff eq cancel left

Stream: general

[Johan Commelin]

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]

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

[Chris Hughes]

rw h does it.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Chris Hughes]

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

[Johan Commelin]

Because you might want to apply it

[Johan Commelin]

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

[Chris Hughes]

I would prefer suffices in that situation. More readable.

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Chris Hughes]

How about apply iff_of_eq (congr_arg _ h)