-- 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) X : W) ((e : (a : V) → W) Y : W))
    (Quiver.homOfEq (X := (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V)) (Y :=
        (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V))
        ((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) X : W) ((e : (a : V) → W) Y : W))
    (Quiver.homOfEq (X := (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) X : W) : V)) (Y :=
        (e : (a : V) → W) ((e.symm : (a : W) → V) ((e : (a : V) → W) Y : W) : V))
        ((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) X : W) ((e : (a : V) → W) Y : W))
⊢ 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))

Tactic:
apply Quiver.homOfEq_injective (X' := e X) (Y' := e Y) (by simp) (by simp)

Premises used: Quiver.homOfEq_injective