-- 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
i j k : D.J
U : Opens (↑(↑(D.V (i, j)) : TopCat) : Type v)
this :
  ∀ (U : (Opens (↑(↑(D.U i) : TopCat) : Type v))ᵒᵖ),
    (D.f i j).c.app U ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫
          NatTrans.app (Hom.c (pullback.snd (D.f i j) (D.f i k))) (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ Eq (α :=
    (D.U i).presheaf.obj (op ((opensFunctor (D.f i j)).obj U)) ⟶
      (Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
        (op ((opensFunctor (D.f i j)).obj U)))
    ((D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)))
    ((D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
      (D.V (i, k)).presheaf.map
        (CategoryStruct.comp (Y :=
          op
            (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
              (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
              (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))))
          (Quiver.Hom.op (X :=
              Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                      (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                  ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
              (Y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)
              (homOfLE (x :=
                Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                          (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                        (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                    ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
                (y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier) ⋯) :
            op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier ⟶
              op
                (Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                        TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                        (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                    (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
                  ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                          TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                          (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                      (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                        (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                    ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)))
          (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.snd (D.f i j) (D.f i k))))
                (eqToHom ⋯ ≫
                  CategoryTheory.Functor.map (Functor.op (Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k)))))
                    (eqToHom ⋯)) ≫
              eqToHom ⋯ :
            op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
                  (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
                  (unop
                    (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k))))
                      (op ((opensFunctor (D.f i j)).obj U))))) ⟶
              (Opens.map (D.f i k).base).op.obj (op ((opensFunctor (D.f i j)).obj U)))))
have h : (D.V (i, k)).presheaf.map
    (CategoryStruct.comp (Y :=
      op
        (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
          (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
          (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
            ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))))))
      (Quiver.Hom.op (X :=
          Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                  TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                  (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
              (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
            ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                    (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
              ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
          (Y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)
          (homOfLE (x :=
            Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                    (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
              ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                    (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier))
            (y := ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier) sorry) :
        op ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier ⟶
          op
            (Set.image (α := (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                    TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                    (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) → (↑(↑(D.V (i, k)) : TopCat) : Type v))
              ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{v}) ↦ C((↑X : Type v), (↑Y : Type v))) (CC :=
                      TopCat.carrier) (X := (↑(pullback (D.f i j) (D.f i k)) : TopCat))
                      (Hom.base (pullback.snd (D.f i j) (D.f i k)))) :
                  (a : (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)) →
                    (↑(↑(D.V (i, k)) : TopCat) : Type v)) ⁻¹'
                ((Opens.map (D.f i k).base).obj (unop (op ((opensFunctor (D.f i j)).obj U)))).carrier)))
      (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.snd (D.f i j) (D.f i k))))
            (eqToHom sorry ≫
              CategoryTheory.Functor.map (Functor.op (Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k)))))
                (eqToHom sorry)) ≫
          eqToHom sorry :
        op
            (Functor.obj (C := Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v))
              (opensFunctor (pullback.snd (D.f i j) (D.f i k)))
              (unop
                (Functor.obj (Functor.op (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k))))
                  (op ((opensFunctor (D.f i j)).obj U))))) ⟶
          (Opens.map (D.f i k).base).op.obj (op ((opensFunctor (D.f i j)).obj U)))) =
  𝟙
    ((Functor.obj (TopCat.Presheaf.pushforward C (D.f i k).base) (D.V (i, k)).presheaf).obj
      (op ((opensFunctor (D.f i j)).obj U)))
Tactic: convert! (Category.comp_id _).symm