-- 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
a : J
𝒲 : (a : J) → OpenCover.{u_2, u} (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).left :=
  fun (a : J) ↦ Precoverage.ZeroHypercover.pullback₁ (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom 𝒰
i : (𝒲 a).I₀
refine_2 :
  ((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i ≫
        CommaMorphism.left
          (OpenCover.glueMorphismsOverOfLocallyDirected.{v_2, u, u_2} 𝒱
            (fun (i : 𝒱.I₀) ↦
              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))
            ⋯ ⋯) =
    pullback.fst (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
      (s.ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ (𝒲 a).f i ≫
      (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) (d.gluedCocone (P := P).ι.app a)).left ≫
        CommaMorphism.left
          (OpenCover.glueMorphismsOverOfLocallyDirected.{v_2, u, u_2} 𝒱
            (fun (i : 𝒱.I₀) ↦
              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))
            ⋯ ⋯) =
    (𝒲 a).f i ≫ (s.ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
simp only [Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover,
      PreZeroHypercover.pullback₁_f, 𝒲, fst_gluedCocone_ι_assoc]

Premises used: CategoryTheory.Precoverage.ZeroHypercover.pullback₁_toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_assoc, CategoryTheory.PreZeroHypercover.pullback₁_f