-- 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
𝒱 : (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 𝒰
a b : J
f : a ⟶ b
refine_2 :
  ∀ (x : (𝒱 a).I₀),
    Eq (α :=
      (𝒱 a).X x ⟶
        (Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.glued (P := P))) b).toComma (P := P) (Q :=
            ⊤) (W := ⊤).left)
      ((𝒱 a).f x ≫
        CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
            (D.map f ≫
              Comma.Hom.mk (P := P) (Q := ⊤) (W := ⊤)
                (OpenCover.glueMorphismsOverOfLocallyDirected.{v_2, u, u_2} (𝒱 b)
                  (fun (i : (𝒱 b).I₀) ↦
                    ((d.cocone (P := P) i).ι.app b).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
                      colimit.ι d.relativeGluingData (P := P).functor i)
                  ⋯ ⋯)
                trivial trivial)))
      ((𝒱 a).f x ≫
        CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
            (Comma.Hom.mk (P := P) (Q := ⊤) (W := ⊤)
                (OpenCover.glueMorphismsOverOfLocallyDirected.{v_2, u, u_2} (𝒱 a)
                  (fun (i : (𝒱 a).I₀) ↦
                    ((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
                      colimit.ι d.relativeGluingData (P := P).functor i)
                  ⋯ ⋯)
                trivial trivial ≫
              CategoryTheory.Functor.map (Functor.obj (Functor.const J) (d.glued (P := P))) f)))
⊢ Eq (α :=
    (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).left ⟶
      (Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.glued (P := P))) b).toComma (P := P) (Q := ⊤)
          (W := ⊤).left)
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (D.map f ≫
          Comma.Hom.mk (P := P) (Q := ⊤) (W := ⊤)
            (OpenCover.glueMorphismsOverOfLocallyDirected.{v_2, u, u_2} (𝒱 b)
              (fun (i : (𝒱 b).I₀) ↦
                ((d.cocone (P := P) i).ι.app b).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
                  colimit.ι d.relativeGluingData (P := P).functor i)
              ⋯ ⋯)
            trivial trivial)))
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (Comma.Hom.mk (P := P) (Q := ⊤) (W := ⊤)
            (OpenCover.glueMorphismsOverOfLocallyDirected.{v_2, u, u_2} (𝒱 a)
              (fun (i : (𝒱 a).I₀) ↦
                ((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
                  colimit.ι d.relativeGluingData (P := P).functor i)
              ⋯ ⋯)
            trivial trivial ≫
          CategoryTheory.Functor.map (Functor.obj (Functor.const J) (d.glued (P := P))) f)))

Tactic:
apply (𝒱 a).hom_ext

Premises used: AlgebraicGeometry.Scheme.Cover.hom_ext