-- Module: Mathlib.AlgebraicGeometry.ColimitsOver
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 𝒰
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
j_1 : J
h :
  Eq (α :=
    (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1).toComma (P :=
          P) (Q := ⊤) (W := ⊤).left ⟶
      (d.cocone (P := P) k).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, u, u_1, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F :=
                (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
            j_1)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i)))
            j_1)
          (d.transitionMap (P := P) (hij ≫ hjk)))))
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, u, u_1, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F :=
                (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
            j_1)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i)))
            j_1)
          (NatTrans.app
              (Iso.hom
                (MorphismProperty.Over.mapComp (P := P) ⊤ ⋯ ⋯ (Cover.trans (P := IsOpenImmersion) 𝒰 (hij ≫ hjk)) ⋯))
              (d.cocone (P := P) i).pt ≫
            CategoryStruct.comp (Y := Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt)
              (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.transitionMap (P := P) hij) :
                Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
                    (Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt) ⟶
                  Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt)
              (d.transitionMap (P := P) hjk :
                Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt ⟶
                  (d.cocone (P := P) k).pt)))))
⊢ Eq (α :=
    ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1 ⟶
      (d.cocone (P := P) k).pt)
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, u, u_1, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
            (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
        j_1)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))) j_1)
      (d.transitionMap (P := P) (hij ≫ hjk)))
    (CategoryStruct.comp (Y :=
      Functor.obj.{v_1, u, u_1, u + 1}
        (Functor.obj (Functor.const J)
          (Cocone.pt (F := (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
            (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
        j_1)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))) j_1)
      (NatTrans.app
          (Iso.hom (MorphismProperty.Over.mapComp (P := P) ⊤ ⋯ ⋯ (Cover.trans (P := IsOpenImmersion) 𝒰 (hij ≫ hjk)) ⋯))
          (d.cocone (P := P) i).pt ≫
        CategoryStruct.comp (Y := Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt)
          (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.transitionMap (P := P) hij) :
            Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt) ⟶
              Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt)
          (d.transitionMap (P := P) hjk :
            Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt ⟶ (d.cocone (P := P) k).pt)))

Tactic:
ext