-- 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
⊢ (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 ⋯ ⋯
have 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) 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)) :
    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 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))
Tactic: apply (he _ _).injective