-- 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.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫
      (D.V (i, j)).presheaf.map (eqToHom ⋯) ≫
        NatTrans.app (Hom.c (pullback.fst (D.f i j) (D.f i k))) (op U) ≫
          invApp (pullback.snd (D.f i j) (D.f i k))
              ((Opens.map (Hom.base (pullback.fst (D.f i j) (D.f i k))) :
                    Opens (↑(↑(D.V (i, j)) : TopCat) : Type v) ⥤
                      Opens (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)).1
                U) ≫
            (D.V (i, k)).presheaf.map (eqToHom ⋯)
have erw : 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) 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)))))
Tactic: erw [(π₁ i, j, k).c.naturality_assoc, reassoc_of% this, ← Functor.map_comp_assoc,
    IsOpenImmersion.inv_naturality_assoc, IsOpenImmersion.app_invApp_assoc, ←
    (D.V (i, k)).presheaf.map_comp, ← (D.V (i, k)).presheaf.map_comp]