-- 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
i : (𝒱 a).I₀
this :
  (𝒱 a).f i ≫ (D.map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫ (𝒱 b).f i
refine_2 :
  Eq (α := (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    ((𝒱 a).f i ≫
      (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) (D.map f)).left ≫
        CommaMorphism.left
          (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)
            ⋯ ⋯))
    ((𝒱 a).f i ≫
      CommaMorphism.left
        (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)
          ⋯ ⋯))
refine_2₁ :
  Eq (α := (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    ((𝒱 a).f i ≫
      (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) (D.map f)).left ≫
        CommaMorphism.left
          (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)
            ⋯ ⋯))
    (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
refine_2₂ :
  Eq (α := (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
            (CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.map f))) ≫
        (𝒱 b).f i ≫
          CommaMorphism.left
            (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)
              ⋯ ⋯) :
      (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
        colimit.ι d.relativeGluingData (P := P).functor i :
      (𝒱 a).X i ⟶ Over.left (d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤)))
refine_2₃ :
  Eq (α := (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
            (CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.map f))) ≫
        ((d.cocone (P := P) i).ι.app b).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
          colimit.ι d.relativeGluingData (P := P).functor i :
      (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
        colimit.ι d.relativeGluingData (P := P).functor i :
      (𝒱 a).X i ⟶ Over.left (d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤)))
refine_2₄ :
  Eq (α := (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (Over.Hom.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
            (CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.map f)) ≫
          ((d.cocone (P := P) i).ι.app b).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)) ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
    (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
refine_2₅ :
  Eq (α := (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (Over.Hom.left
          (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤)
            (CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.map f) ≫
              (d.cocone (P := P) i).ι.app b)) ≫
        colimit.ι d.relativeGluingData (P := P).functor i :
      Over.left
          ((Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) (D.obj a)).toComma (P := P) (Q := ⊤) (W := ⊤)) ⟶
        d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
refine_2₆ :
  Eq (α := (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (Over.Hom.left
        (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤)
          ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).map f ≫ (d.cocone (P := P) i).ι.app b)) ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
    (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
refine_2₇ refine_2₈ :
  Eq (α := (𝒱 a).X i ⟶ d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (Over.Hom.left (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) ((d.cocone (P := P) i).ι.app a)) ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
    (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i)
⊢ (𝒱 a).f i ≫
      (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) (D.map f)).left ≫
        CommaMorphism.left
          (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)
            ⋯ ⋯) =
    (𝒱 a).f i ≫
      CommaMorphism.left
          (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)
            ⋯ ⋯) ≫
        𝟙 d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
rw [Category.comp_id, Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left,
      reassoc_of% this, Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left,
      ← Over.comp_left_assoc, ← Comma.comp_hom, ← Functor.comp_map, Cocone.w]

Premises used: CategoryTheory.Over.comp_left_assoc, AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left, CategoryTheory.Category.comp_id, CategoryTheory.Limits.Cocone.w, CategoryTheory.MorphismProperty.Comma.comp_hom, CategoryTheory.Functor.comp_map