-- Lean 4 proof step from Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : GlueData.{v, u} C
inst_1 : HasLimits.{v, u} C
i j k : D.J
U : Opens (↑(↑(D.U i) : TopCat) : Type v)
⊢ Eq (α :=
    (D.U i).presheaf.obj (op U) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (D.f j k).base) (D.V (j, k)).presheaf).obj
        (op
          (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
            (Opens.map (Hom.base (D.ι j)) :
              Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U j) : TopCat) : Type v))
            (Functor.obj
                (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) ⋯ :
                  Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
                U :
              Opens (↑(↑D.glued : TopCat) : Type v)))))
    (CategoryStruct.comp (Y :=
      (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f j i) (D.f j k))))
            (pullback (D.f j i) (D.f j k)).presheaf).obj
        (op ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))))
      (NatTrans.app (Hom.c (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) (op U) :
        (D.U i).presheaf.obj (op U) ⟶
          (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)))
                (pullback (D.f j i) (D.f j k)).presheaf).obj
            (op U))
      (invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (Hom.base (pullback.fst (D.f j i) (D.f j k))) :
                Opens (↑(↑(D.V (j, i)) : TopCat) : Type v) ⥤
                  Opens (↑(↑(pullback (D.f j i) (D.f j k)) : TopCat) : Type v)).1
            ((Opens.map (D.t j i).base).1 (unop ((Opens.map (D.f i j).base).op.obj (op U))))) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯ ≫ (Opens.map (D.f j k).base).op.map (Quiver.Hom.op (eqToHom ⋯)))))
    (CategoryStruct.comp (Y :=
      (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)))
            (pullback (D.f j i) (D.f j k)).presheaf).obj
        (op U))
      (NatTrans.app (Hom.c (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) (op U))
      (invApp (pullback.snd (D.f j i) (D.f j k))
          ((Opens.map (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑(pullback (D.f j i) (D.f j k)) : TopCat) : Type v)).1
            U) ≫
        (D.V (j, k)).presheaf.map (eqToHom ⋯)))
have h : Eq (α :=
  (D.U i).presheaf.obj (op U) ⟶
    (Functor.obj (TopCat.Presheaf.pushforward C (D.f j k).base) (D.V (j, k)).presheaf).obj
      (op
        (Functor.obj (C := Opens (↑(↑D.glued : TopCat) : Type v))
          (Opens.map (Hom.base (D.ι j)) : Opens (↑(↑D.glued : TopCat) : Type v) ⥤ Opens (↑(↑(D.U j) : TopCat) : Type v))
          (Functor.obj
              (IsOpenEmbedding.functor (f := Hom.base (D.ι i)) sorry :
                Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑D.glued : TopCat) : Type v))
              U :
            Opens (↑(↑D.glued : TopCat) : Type v)))))
  (CategoryStruct.comp (Y :=
    (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f j i) (D.f j k))))
          (pullback (D.f j i) (D.f j k)).presheaf).obj
      (op ((Opens.map (D.t j i).base).1 ((Opens.map (D.f i j).base).obj U))))
    (NatTrans.app (Hom.c (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) (op U) :
      (D.U i).presheaf.obj (op U) ⟶
        (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)))
              (pullback (D.f j i) (D.f j k)).presheaf).obj
          (op U))
    (invApp (pullback.snd (D.f j i) (D.f j k))
        ((Opens.map (Hom.base (pullback.fst (D.f j i) (D.f j k))) :
              Opens (↑(↑(D.V (j, i)) : TopCat) : Type v) ⥤
                Opens (↑(↑(pullback (D.f j i) (D.f j k)) : TopCat) : Type v)).1
          ((Opens.map (D.t j i).base).1 ((Opens.map (D.f i j).base).obj U))) ≫
      (D.V (j, k)).presheaf.map (eqToHom sorry ≫ Quiver.Hom.op ((Opens.map (D.f j k).base).map (eqToHom sorry)))))
  (CategoryStruct.comp (Y :=
    (Functor.obj (TopCat.Presheaf.pushforward C (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)))
          (pullback (D.f j i) (D.f j k)).presheaf).obj
      (op U))
    (NatTrans.app (Hom.c (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) (op U))
    (invApp (pullback.snd (D.f j i) (D.f j k))
        ((Opens.map (Hom.base (pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j)) :
              Opens (↑(↑(D.U i) : TopCat) : Type v) ⥤ Opens (↑(↑(pullback (D.f j i) (D.f j k)) : TopCat) : Type v)).1
          U) ≫
      (D.V (j, k)).presheaf.map (eqToHom sorry)))
Tactic: dsimp only [Functor.op, unop_op, Quiver.Hom.unop_op]