awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : J
i : (𝒱 a).I₀
⊢ (((d.cocone (P := P) i).ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left ≫
        colimit.ι d.relativeGluingData (P := P).functor i) ≫
      Over.hom
        ((Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.glued (P := P))) a).toComma (P := P) (Q :=
          ⊤) (W := ⊤)) =
    (𝒱 a).f i ≫ Over.hom ((D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤))

Tactic:
simp [𝒱, pullback.condition, glued]

Premises used: CategoryTheory.Limits.pullback.condition, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.glued
-- 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 :
  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)))
⊢ Eq (α := D.obj a ⟶ Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.glued (P := P))) b)
    (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)
    (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:
ext
-- 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₀
⊢ (𝒱 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

Tactic:
simp [𝒱]
-- 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₀
⊢ (𝒱 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

Tactic:
have : (𝒱 a).f i ≫ (D.map f).left =
        ((D ⋙ Over.pullback _ _ (𝒰.f i)).map f).left ≫ (𝒱 b).f i := by
      simp [𝒱]
-- 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
refine_1 : (s : Cocone D) → d.gluedCocone (P := P).pt ⟶ s.pt
refine_2 :
  ∀ (s : Cocone D) (j : J),
    d.gluedCocone (P := P).ι.app j ≫
        Comma.Hom.mk (P := P) (Q := ⊤) (W := ⊤)
          (OpenCover.glueMorphismsOverOfLocallyDirected.{v_2, u, u_2} 𝒱
            (fun (i : 𝒱.I₀) ↦
              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)))
            ⋯ ⋯)
          trivial trivial =
      s.ι.app j
refine_3 :
  ∀ (s : Cocone D) (m : d.gluedCocone (P := P).pt ⟶ s.pt),
    (∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j) →
      m =
        Comma.Hom.mk (P := P) (Q := ⊤) (W := ⊤)
          (OpenCover.glueMorphismsOverOfLocallyDirected.{v_2, u, u_2} 𝒱
            (fun (i : 𝒱.I₀) ↦
              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)))
            ⋯ ⋯)
          trivial trivial
⊢ IsColimit (d.gluedCocone (P := P))

Tactic:
refine { desc s := ?_, fac := ?_, uniq := ?_ }
-- 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
refine_1 : (i : 𝒱.I₀) → 𝒱.X i ⟶ Over.left (s.pt.toComma (P := P) (Q := ⊤) (W := ⊤))
refine_1₁ :
  ∀ {i j : 𝒱.I₀} (hij : i ⟶ j),
    Eq (α := 𝒱.X i ⟶ Over.left (s.pt.toComma (P := P) (Q := ⊤) (W := ⊤)))
      (Cover.trans (P := IsOpenImmersion) 𝒱 hij ≫
        CategoryStruct.comp (Y :=
          (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
                  (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s)).toComma
              (P := P) (Q := ⊤) (W := ⊤).left)
          (CommaMorphism.left
            (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
              ((d.isColimit (P := P) j).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s))))
          (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))
      (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)))
refine_1₂ :
  ∀ (i : 𝒱.I₀),
    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 := ⊤))
⊢ d.gluedCocone (P := P).pt ⟶ s.pt

Tactic:
refine ⟨𝒱.glueMorphismsOverOfLocallyDirected ?_ ?_ ?_, trivial, trivial⟩
-- 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₀
⊢ 𝒱.X i ⟶ Over.left (s.pt.toComma (P := P) (Q := ⊤) (W := ⊤))

Tactic:
exact ((d.isColimit i).desc (Functor.mapCocone _ s)).left ≫ pullback.fst _ _

Premises used: CategoryTheory.Functor.mapCocone, CategoryTheory.CommaMorphism.left, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.Limits.pullback.fst, CategoryTheory.MorphismProperty.Comma.Hom.toCommaMorphism, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimit
-- 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 j : 𝒱.I₀
hij : i ⟶ j
⊢ Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
      Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
        (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s))
    (d.transitionMap (P := P) hij ≫
        (d.isColimit (P := P) j).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s) :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s))
    (CategoryStruct.comp (Y :=
        Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
          (Cocone.pt (F := D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i))
            (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)))
        (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯)
          ((d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)))
        (NatTrans.app
          (Over.pullbackMapHomPullback (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial (𝒰.f j)
            (𝒰.f i) ⋯)
          s.pt) :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) s.pt)

Tactic:
have : d.transitionMap hij ≫ (d.isColimit j).desc ((Over.pullback P ⊤ (𝒰.f j)).mapCocone s) =
          (Over.map ⊤ (d.prop_trans hij)).map
            ((d.isColimit i).desc ((MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).mapCocone s)) ≫
          (Over.pullbackMapHomPullback _ (d.prop_trans hij) trivial _ _).app _ := by
        apply (isColimitOfPreserves (Over.map ⊤ <| d.prop_trans _) (d.isColimit i)).hom_ext
        intro
        ext
        apply pullback.hom_ext <;> simp [cocone_ι_transitionMap_assoc, ← Functor.map_comp_assoc]
-- 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₀
⊢ 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

Tactic:
have : _ ≫ pullback.snd _ _ = _ := Over.w ((d.isColimit i).desc (Functor.mapCocone _ s))
-- 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 :
  (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom ≫ 𝒰.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.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 ⋯))

Tactic:
rw [reassoc_of% this]
-- 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
⊢ (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom ≫ 𝒰.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 ⋯))

Tactic:
simp