-- Module: Mathlib.CategoryTheory.Category.Quiv
Goal:
V W : Type u
inst : Quiver.{u_1, u} V
inst_1 : Quiver.{u_1, u} W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W)
X Y : (↑(of V) : Type u)
f : X ⟶ Y
a :
  Eq (α :=
    Quiver.Hom (V := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V) : W)
      ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V) : W))
    ((he ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W)) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W)) :
          (a : (e.symm : (a : W) → V) ((e : (a : V) → W) X) ⟶ (e.symm : (a : W) → V) ((e : (a : V) → W) Y)) →
            (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X)) ⟶
              (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y)))
        ((Equiv.symm
                (he ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W))
                  ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W))) :
              (a :
                  (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X)) ⟶
                    (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y))) →
                (e.symm : (a : W) → V) ((e : (a : V) → W) X) ⟶ (e.symm : (a : W) → V) ((e : (a : V) → W) Y))
            (Quiver.homOfEq ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) f) ⋯ ⋯ :
              Quiver.Hom (V := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V) : W)
                ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V) : W)) :
          Quiver.Hom (V := V) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V)
            ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V)) :
      Quiver.Hom (V := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V) : W)
        ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V) : W))
    ((he ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W)) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W)) :
          (a : (e.symm : (a : W) → V) ((e : (a : V) → W) X) ⟶ (e.symm : (a : W) → V) ((e : (a : V) → W) Y)) →
            (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X)) ⟶
              (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y)))
        (Quiver.homOfEq f ⋯ ⋯) :
      Quiver.Hom (V := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V) : W)
        ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V) : W))
⊢ (Equiv.symm
          (he ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W)) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W))) :
        (a :
            (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X)) ⟶
              (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y))) →
          (e.symm : (a : W) → V) ((e : (a : V) → W) X) ⟶ (e.symm : (a : W) → V) ((e : (a : V) → W) Y))
      (Quiver.homOfEq ((he X Y : (a : X ⟶ Y) → (e : (a : V) → W) X ⟶ (e : (a : V) → W) Y) f) ⋯ ⋯ :
        Quiver.Hom (V := W) ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V) : W)
          ((e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V) : W)) =
    Quiver.homOfEq f ⋯ ⋯

Tactic:
apply (he _ _).injective

Premises used: Equiv.injective