Sum.elim equality

Stream: mathlib4

[Martin Dvořák]

It seems to me that we either miss a lemma or a simp tag...

import Mathlib

example {α β γ : Type*} {u u' : α → γ} {v v' : β → γ}
    (huv : Sum.elim u v = Sum.elim u' v') :
    v = v' := by
  simp_all [Function.funext_iff]

[Eric Wieser]

That lemma can't be simp, it would try to apply on any function equality

[Eric Wieser]

I think you probably want Sum.elim u v = Sum.elim u' v' \iff u = u' \and v = v'?

[Martin Dvořák]

Yes.

[Martin Dvořák]

If this lemma is really missing (it is not just my overlook), std deserves it IMO.

[Martin Dvořák]

https://github.com/leanprover/std4/issues/685