-- 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))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone (P := P) i).pt ≅
  Cocone.pt (F :=
    (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) ⋙
      MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
    (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.cocone (P := P) j)) :=
  (d.isColimit (P := P) i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.isColimit (P := P) j))
    (D.isoWhiskerLeft
        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝒰.f j) (𝒰.f i)
          ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm)
a : J
h :
  Eq (α :=
    (Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
              (Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.obj a))).toComma
          (P := P) (Q := ⊤) (W := ⊤).left ⟶
      (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
          (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯)
              ((D.isoWhiskerLeft
                        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij)
                          (𝒰.f j) (𝒰.f i) ⋯) ≪≫
                      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm).hom.app
                a) ≫
            NatTrans.app
                (Adjunction.counit
                  (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial))
                ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).obj a) ≫
              (d.cocone (P := P) j).ι.app a)) :
      (Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.obj a))).toComma
            (P := P) (Q := ⊤) (W := ⊤).left ⟶
        (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
          (NatTrans.app (d.trans (P := P) hij) a ≫ (d.cocone (P := P) j).ι.app a)) :
      (Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.obj a))).toComma
            (P := P) (Q := ⊤) (W := ⊤).left ⟶
        (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)
⊢ Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
        (Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.obj a)) ⟶
      (d.cocone (P := P) j).pt)
    (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯)
          ((D.isoWhiskerLeft
                    (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij)
                      (𝒰.f j) (𝒰.f i) ⋯) ≪≫
                  (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                      (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm).hom.app
            a) ≫
        NatTrans.app
            (Adjunction.counit
              (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial))
            ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)).obj a) ≫
          (d.cocone (P := P) j).ι.app a :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
          (Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.obj a)) ⟶
        (d.cocone (P := P) j).pt)
    (NatTrans.app (d.trans (P := P) hij) a ≫ (d.cocone (P := P) j).ι.app a :
      (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj a ⟶
        Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.cocone (P := P) j).pt) a)

Tactic:
ext