-- 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 (↑(↑(pullback (D.f i j) (D.f i k)) : TopCat) : Type v)
⊢ Eq (α :=
    (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ⟶
      (D.V (k, i)).presheaf.obj
        (op
          (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
            (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U))))
    ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
      (D.V (k, i)).presheaf.map (eqToHom ⋯))
    ((CategoryStruct.comp (Y :=
          (pullback (D.f k i) (D.f k j)).presheaf.obj
            (op
              (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))))
          ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
            NatTrans.app (Hom.c (pullback.fst (D.f k i) (D.f k j)))
              (op ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))
          ((pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom ⋯)) ≫
        (pullback (D.f k i) (D.f k j)).presheaf.map
          (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom ⋯))))) ≫
      invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U))
have h : Eq (α :=
  (D.V (i, k)).presheaf.obj (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ⟶
    (D.V (k, i)).presheaf.obj
      (op
        (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
          (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U))))
  ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
    (D.V (k, i)).presheaf.map (eqToHom sorry))
  ((D.t k i).c.app (op (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)) ≫
    CategoryStruct.comp (Y :=
      (pullback (D.f k i) (D.f k j)).presheaf.obj
        (op
          (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
            ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))))
      (NatTrans.app (Hom.c (pullback.fst (D.f k i) (D.f k j)))
        (op ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U))))
      (CategoryStruct.comp (Y :=
        (pullback (D.f k i) (D.f k j)).presheaf.obj
          (op
            ((Opens.map (D.t' k i j).base).obj
              (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))))
        ((pullback (D.f k i) (D.f k j)).presheaf.map (eqToHom sorry) :
          (pullback (D.f k i) (D.f k j)).presheaf.obj
              (op
                (Functor.obj (Opens.map (Hom.base (pullback.fst (D.f k i) (D.f k j))))
                  ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))) ⟶
            (pullback (D.f k i) (D.f k j)).presheaf.obj
              (op
                ((Opens.map (D.t' k i j).base).obj
                  (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                    (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))))
        ((pullback (D.f k i) (D.f k j)).presheaf.map
              (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom sorry)))) ≫
            invApp (pullback.fst (D.f k i) (D.f k j)) ((Opens.map (D.t' k i j).base).1 U) :
          (pullback (D.f k i) (D.f k j)).presheaf.obj
              (op
                ((Opens.map (D.t' k i j).base).obj
                  (Functor.obj (Opens.map (Hom.base (pullback.snd (D.f i j) (D.f i k))))
                    (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)))) ⟶
            (D.V (k, i)).presheaf.obj
              (op
                (Functor.obj (C := Opens (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v))
                  (opensFunctor (pullback.fst (D.f k i) (D.f k j))) ((Opens.map (D.t' k i j).base).1 U))))))
Tactic: simp_rw [Category.assoc]