-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (hypothesis)
Goal:
P : MorphismProperty Scheme
inst : P.IsStableUnderBaseChange
inst_1 : P.IsMultiplicative
S : Scheme
J : Type u_1
inst_2 : Category.{v_1, u_1} J
D : CategoryTheory.Functor.{v_1, u, u_1, u + 1} J (P.Over ⊤ S)
𝒰 : OpenCover.{u_2, u} S
inst_3 : Category.{v_2, u_2} 𝒰.I₀
inst_4 : LocallyDirected.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰
d : ColimitGluingData.{v_2, u, v_1, u_1, u_2} (P := P) D 𝒰
inst_5 :
  ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
    PreservesColimitsOfShape.{v_1, u_1, u, u, u + 1, u + 1} (C := P.Over ⊤ (𝒰.X j)) J
      (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
inst_6 : Quiver.IsThin.{u_2, v_2} 𝒰.I₀
inst_7 : Small.{u, u_2} 𝒰.I₀
inst_8 : IsZariskiLocalAtTarget P
𝒱 : OpenCover.{u_2, u} d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left := d.relativeGluingData (P := P).cover
s : Cocone D
i j : 𝒱.I₀
hij : i ⟶ j
⊢ Eq (α :=
    (Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt).toComma (P := P) (Q := ⊤) (W :=
          ⊤).left ⟶
      Over.left (s.pt.toComma (P := P) (Q := ⊤) (W := ⊤)))
    (CommaMorphism.left (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤) (d.transitionMap (P := P) hij)) ≫
        CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
          (CommaMorphism.left
              (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
                ((d.isColimit (P := P) j).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s))) :
            (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left ⟶
              (Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s.pt).toComma (P := P) (Q := ⊤) (W := ⊤).left)
          (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j) :
            pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j) ⟶
              s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).left) :
      (Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt).toComma (P := P) (Q := ⊤) (W :=
            ⊤).left ⟶
        Over.left (s.pt.toComma (P := P) (Q := ⊤) (W := ⊤)))
    (CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
        (CommaMorphism.left
            (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
              ((d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s))) :
          (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left ⟶
            (Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s.pt).toComma (P := P) (Q := ⊤) (W := ⊤).left)
        (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) :
          pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ⟶ s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).left) :
      𝒱.X i ⟶ Over.left (s.pt.toComma (P := P) (Q := ⊤) (W := ⊤)))
have this : Eq (α :=
  Functor.obj (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i).pt ⟶
    Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
      (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s))
  (d.transitionMap (P := P) hij ≫
      (d.isColimit (P := P) j).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s) :
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i).pt ⟶
      Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
        (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s))
  (CategoryStruct.comp (Y :=
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ sorry)
        (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i))
          (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)))
      (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ sorry)
        ((d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)))
      (NatTrans.app
        (Over.pullbackMapHomPullback (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) sorry trivial (𝒰.f j)
          (𝒰.f i) sorry)
        s.pt) :
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i).pt ⟶
      Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s.pt)
Tactic: have : d.transitionMap hij ≫ (d.isColimit j).desc ((Over.pullback P ⊤ (𝒰.f j)).mapCocone s) =
          (Over.map ⊤ (d.prop_trans hij)).map
            ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)) ≫
          (Over.pullbackMapHomPullback _ (d.prop_trans hij) trivial _ _).app _ := by
        apply (isColimitOfPreserves (Over.map ⊤ <| d.prop_trans _) (d.isColimit i)).hom_ext
        intro
        ext
        apply pullback.hom_ext <;> simp [cocone_ι_transitionMap_assoc, ← Functor.map_comp_assoc]