Injectivity of equivalences

Stream: Is there code for X?

[Jeremy Tan]

Do we have these two lemmas?

lemma trans_injective_right {α β γ : Type*} {e₁ : α ≃ β} {e₂ e₃ : β ≃ γ}
    (h : e₁.trans e₂ = e₁.trans e₃) : e₂ = e₃ := by
  simp_rw [Equiv.ext_iff, trans_apply] at h
  ext y; obtain ⟨x', hx'⟩ := e₁.surjective y; subst hx'; exact h x'

lemma trans_injective_left {α β γ : Type*} {e₁ e₂ : α ≃ β} {e₃ : β ≃ γ}
    (h : e₁.trans e₃ = e₂.trans e₃) : e₁ = e₂ := by
  simp_rw [Equiv.ext_iff, trans_apply] at h
  ext y; exact e₃.injective (h y)

[Markus Himmel]

import Mathlib.Logic.Equiv.Defs

lemma trans_injective_right {α β γ : Type*} {e₁ : α ≃ β} {e₂ e₃ : β ≃ γ}
    (h : e₁.trans e₂ = e₁.trans e₃) : e₂ = e₃ :=
  (Equiv.equivCongr e₁.symm (Equiv.refl _)).injective h

lemma trans_injective_left {α β γ : Type*} {e₁ e₂ : α ≃ β} {e₃ : β ≃ γ}
    (h : e₁.trans e₃ = e₂.trans e₃) : e₁ = e₂ :=
  (Equiv.equivCongr (Equiv.refl _) e₃).injective h

[Eric Wieser]

These should be started with Injective