-- 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 : 𝒱.I₀
this :
  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 ⟶
          (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i))
                  (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)).toComma
              (P := P) (Q := ⊤) (W := ⊤).left)
      (pullback.snd s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)) =
    (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom
refine_1 :
  CategoryStruct.comp (Y :=
      (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i))
              (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)).toComma
          (P := P) (Q := ⊤) (W := ⊤).left)
      (CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
          ((d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s))))
      (pullback.snd s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫ 𝒰.f i) =
    PreZeroHypercover.f (Precoverage.ZeroHypercover.toPreZeroHypercover d.relativeGluingData (P := P).cover) i ≫
      Over.hom
        (Comma.toComma (P := P) (Q := ⊤) (W := ⊤)
          (MorphismProperty.Over.mk (P := P) ⊤ (A := d.relativeGluingData (P := P).glued)
            d.relativeGluingData (P := P).toBase ⋯))
⊢ CategoryStruct.comp (Y :=
        (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i))
                (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)).toComma
            (P := P) (Q := ⊤) (W := ⊤).left)
        (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
            ((d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s))))
        (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)) ≫
      Over.hom (s.pt.toComma (P := P) (Q := ⊤) (W := ⊤)) =
    𝒱.f i ≫ Over.hom (d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤))

Tactic:
simp only [glued, Category.assoc, 𝒱, pullback.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued