-- 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 𝒰
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
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 ⟶
      Functor.obj (𝟭 Scheme) s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
      (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 ≫
                (d.isColimit (P := P) j).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)))) :
        (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1).toComma
              (P := P) (Q := ⊤) (W := ⊤).left ⟶
          (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                  (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)).toComma
              (P := P) (Q := ⊤) (W := ⊤).left)
      (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))
    (CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
      (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)
              (CategoryStruct.comp (Y :=
                Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
                  (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) ⊤ ⋯)
                  ((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) ⋯ trivial
                    (𝒰.f j) (𝒰.f i) ⋯)
                  s.pt)))) :
        (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1).toComma
              (P := P) (Q := ⊤) (W := ⊤).left ⟶
          (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                  (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)).toComma
              (P := P) (Q := ⊤) (W := ⊤).left)
      (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))
h₁ :
  Eq (α :=
    (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1).toComma (P :=
          P) (Q := ⊤) (W := ⊤).left ⟶
      𝒰.X j)
    (CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
      (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 ≫
                (d.isColimit (P := P) j).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)))) :
        (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1).toComma
              (P := P) (Q := ⊤) (W := ⊤).left ⟶
          (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                  (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)).toComma
              (P := P) (Q := ⊤) (W := ⊤).left)
      (pullback.snd s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))
    (CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
      (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)
              (CategoryStruct.comp (Y :=
                Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
                  (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) ⊤ ⋯)
                  ((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) ⋯ trivial
                    (𝒰.f j) (𝒰.f i) ⋯)
                  s.pt)))) :
        (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1).toComma
              (P := P) (Q := ⊤) (W := ⊤).left ⟶
          (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                  (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)).toComma
              (P := P) (Q := ⊤) (W := ⊤).left)
      (pullback.snd s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))
⊢ Eq (α :=
    (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1).toComma (P :=
          P) (Q := ⊤) (W := ⊤).left ⟶
      (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
              (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)).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 ≫
            (d.isColimit (P := P) j).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)))))
    (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)
          (CategoryStruct.comp (Y :=
            Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
              (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) ⊤ ⋯)
              ((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) ⋯ trivial
                (𝒰.f j) (𝒰.f i) ⋯)
              s.pt)))))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext