-- 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 ⋯)
⊢ (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)))) =
    𝟙
      ((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)))
have h : Eq.{v + 1} (α :=
  (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)) ⟶
    (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.V (i, k)).presheaf.obj (op ((Opens.map (D.f i k).base).obj (unop (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: erw [(D.V (i, k)).presheaf.map_id]