-- 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 ⋯))
    ((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 ⋯) :
            (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 ⋯)))) ≫
              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))))))
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 :=
      (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)))
            (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.V (k, i)).presheaf.map
          (Quiver.Hom.op (X :=
            Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : 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 k i) (D.f k j)) : TopCat))
                    (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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 k i) (D.f k j)) : TopCat))
                      (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                  (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
                    (↑(↑(D.V (k, i)) : TopCat) : Type v)) ⁻¹'
                ((Opens.map (D.t k i).base).obj
                    (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier))
            (Y :=
            ((Opens.map (D.t k i).base).obj (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier)
            (eqToHom (X :=
              Set.image (α := (↑(↑(pullback (D.f k i) (D.f k j)) : 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 k i) (D.f k j)) : TopCat))
                      (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                  (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) → (↑(↑(D.V (k, i)) : 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 k i) (D.f k j)) : TopCat))
                        (Hom.base (pullback.fst (D.f k i) (D.f k j)))) :
                    (a : (↑(↑(pullback (D.f k i) (D.f k j)) : TopCat) : Type v)) →
                      (↑(↑(D.V (k, i)) : TopCat) : Type v)) ⁻¹'
                  ((Opens.map (D.t k i).base).obj
                      (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier))
              (Y :=
              ((Opens.map (D.t k i).base).obj
                  (Functor.obj (opensFunctor (pullback.snd (D.f i j) (D.f i k))) U)).carrier)
              sorry)) :
        (D.V (k, i)).presheaf.obj
            (op ((Opens.map (D.t k i).base).obj (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)))
                (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))))))
      (CategoryStruct.comp (Y :=
          (D.V (k, i)).presheaf.obj
            (op
              (Functor.obj (opensFunctor (pullback.fst (D.f k i) (D.f k j)))
                (unop
                  (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.map
            (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.fst (D.f k i) (D.f k j)))) (eqToHom sorry)))
          ((D.V (k, i)).presheaf.map
            (CategoryTheory.Functor.map (Functor.op (opensFunctor (pullback.fst (D.f k i) (D.f k j))))
              (Quiver.Hom.op ((Opens.map (D.t' k i j).base).map (Quiver.Hom.unop (eqToHom sorry)))))) :
        (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)))
                (unop
                  (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.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: rw [IsOpenImmersion.inv_naturality, IsOpenImmersion.inv_naturality_assoc,
      IsOpenImmersion.app_inv_app'_assoc]