-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Quiv (goal)
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
⊢ 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))
have 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) sorry sorry :
              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)))
      sorry sorry :
    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 sorry sorry))
      sorry sorry :
    Quiver.Hom (V := W) ((e : (a : V) → W) X : W) ((e : (a : V) → W) Y : W))
Tactic: apply Quiver.homOfEq_injective (X' := e X) (Y' := e Y) (by simp) (by simp)