Sum.elim injectivity

Stream: Is there code for X?

[Martin Dvořák]

I cannot find a lemma for this:

import Mathlib

example {α β γ : Type} (u u' : α → γ) (v v' : β → γ) (hyp : Sum.elim u v = Sum.elim u' v') :
    u = u' := by
  sorry

[Martin Dvořák]

Also this:

import Mathlib

lemma sumElim_le_sumElim_iff {α β γ : Type} [LE γ] (u u' : α → γ) (v v' : β → γ) :
    Sum.elim u v ≤ Sum.elim u' v' ↔ u ≤ u' ∧ v ≤ v' := by
  constructor <;> intro hyp
  · constructor
    · intro a
      have hypa := hyp (Sum.inl a)
      rwa [Sum.elim_inl, Sum.elim_inl] at hypa
    · intro b
      have hypb := hyp (Sum.inr b)
      rwa [Sum.elim_inr, Sum.elim_inr] at hypb
  · intro i
    cases i with
    | inl a =>
      rw [Sum.elim_inl, Sum.elim_inl]
      exact hyp.left a
    | inr b =>
      rw [Sum.elim_inr, Sum.elim_inr]
      exact hyp.right b

Should I PR it? I didn't find it in the libraries.

[Eric Rodriguez]

example {α β γ : Type} (u u' : α → γ) (v v' : β → γ) (hyp : Sum.elim u v = Sum.elim u' v') :
    u = u' := funext (fun x ↦ congr_fun hyp (.inl x))

-- weird that this fails:
example {α β γ : Type} (u u' : α → γ) (v v' : β → γ) (hyp : Sum.elim u v = Sum.elim u' v') :
    u = u' := funext (fun x ↦ congr($hyp (Sum.inl x))) -- function expected `x α β`

lemma sumElim_le_sumElim_iff {α β γ : Type} [LE γ] (u u' : α → γ) (v v' : β → γ) :
    Sum.elim u v ≤ Sum.elim u' v' ↔ u ≤ u' ∧ v ≤ v' := by
  simp only [Pi.le_def]
  aesop

[Yaël Dillies]

You could add Sum.elim_inj, Sum.elim_le_elim, Sum.elim_lt_elim, yes.

[Martin Dvořák]

Something like the following code should go to Mathlib?

import Mathlib

lemma Sum.elim_inj {α β γ : Type*} (u u' : α → γ) (v v' : β → γ) :
    Sum.elim u v = Sum.elim u' v' ↔ u = u' ∧ v = v' :=
  ⟨fun hyp => ⟨funext (fun x ↦ congr_fun hyp (.inl x)), funext (fun x ↦ congr_fun hyp (.inr x))⟩, by aesop⟩

lemma Sum.elim_le_elim {α β γ : Type*} [LE γ] (u u' : α → γ) (v v' : β → γ) :
    Sum.elim u v ≤ Sum.elim u' v' ↔ u ≤ u' ∧ v ≤ v' := by
  simp only [Pi.le_def]
  aesop

I was unsuccessful in proving the former lemma in the same style as the latter lemma.