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
𝒱 : OpenCover.{u_2, u} d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left := d.relativeGluingData (P := P).cover
s : Cocone D
m : d.gluedCocone (P := P).pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
h :
  CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
      ((Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) ((d.cocone (P := P) i).ι.app a)).left ≫
        CommaMorphism.left (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) (Iso.inv (d.pullbackGluedIso (P := P) i))) ≫
          pullback.lift
            (pullback.fst d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
              m.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left)
            (pullback.snd d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)) ⋯)
      (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)) =
    CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
      (pullback.lift
        (pullback.fst (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
          (s.ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left)
        (pullback.snd (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)) ⋯)
      (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
⊢ ((d.cocone (P := P) i).ι.app a ≫
              Iso.inv (d.pullbackGluedIso (P := P) i) ≫
                CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) m).toCommaMorphism
          (P := P) (Q := ⊤) (W := ⊤).left ≫
      pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) =
    CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
      (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)) a)) :
        ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).obj a).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) ⟶
          Functor.obj (𝟭 Scheme) s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)

Tactic:
dsimp
-- 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
m : d.gluedCocone (P := P).pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
h :
  (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) ((d.cocone (P := P) i).ι.app a)).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i ≫ m.toCommaMorphism (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
⊢ CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
      ((Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) ((d.cocone (P := P) i).ι.app a)).left ≫
        CommaMorphism.left (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) (Iso.inv (d.pullbackGluedIso (P := P) i))) ≫
          pullback.lift
            (pullback.fst d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
              m.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left)
            (pullback.snd d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)) ⋯)
      (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)) =
    CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
      (pullback.lift
        (pullback.fst (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
          (s.ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left)
        (pullback.snd (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)) ⋯)
      (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))

Tactic:
simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          pullbackGluedIso_inv_fst_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.PullbackCone.mk_π_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.pullbackGluedIso_inv_fst_assoc, CategoryTheory.Limits.limit.lift_π
-- 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
m : d.gluedCocone (P := P).pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
h :
  (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) ((d.cocone (P := P) i).ι.app a)).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i ≫ m.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    pullback.fst (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
      (d.gluedCocone (P := P).ι.app a ≫ m).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
⊢ (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) ((d.cocone (P := P) i).ι.app a)).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i ≫ m.toCommaMorphism (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

Tactic:
rw [← congr($(hm a).left)]
-- 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
m : d.gluedCocone (P := P).pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ (Comma.Hom.hom (P := P) (Q := ⊤) (W := ⊤) ((d.cocone (P := P) i).ι.app a)).left ≫
      colimit.ι d.relativeGluingData (P := P).functor i ≫ m.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    pullback.fst (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ≫
      (d.gluedCocone (P := P).ι.app a ≫ m).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left

Tactic:
simp [fst_gluedCocone_ι_assoc]

Premises used: AlgebraicGeometry.Scheme.Cover.ColimitGluingData.fst_gluedCocone_ι_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
m : d.gluedCocone (P := P).pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
a : J
⊢ ((d.cocone (P := P) i).ι.app a ≫
              Iso.inv (d.pullbackGluedIso (P := P) i) ≫
                CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) m).toCommaMorphism
          (P := P) (Q := ⊤) (W := ⊤).left ≫
      pullback.snd s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) =
    CategoryStruct.comp (Y := pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
      (CommaMorphism.left
          (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
            (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)) a)) :
        ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).obj a).toComma (P := P) (Q := ⊤) (W := ⊤).left ⟶
          (Functor.obj (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s.pt).toComma (P := P) (Q := ⊤) (W := ⊤).left)
      (pullback.snd s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) :
        pullback s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ⟶ 𝒰.X 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
𝒱 : OpenCover.{u_2, u} d.glued (P := P).toComma (P := P) (Q := ⊤) (W := ⊤).left := d.relativeGluingData (P := P).cover
s : Cocone D
m : d.gluedCocone (P := P).pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
⊢ Iso.inv (d.pullbackGluedIso (P := P) i) ≫ CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) m =
    (d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)

Tactic:
have : (d.pullbackGluedIso i).inv ≫ (Over.pullback P ⊤ (𝒰.f i)).map m =
        (d.isColimit i).desc ((Over.pullback P ⊤ (𝒰.f i)).mapCocone s) := by
      refine (d.isColimit i).hom_ext fun a ↦ ?_
      rw [IsColimit.fac]
      ext
      apply pullback.hom_ext
      · dsimp
        simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          pullbackGluedIso_inv_fst_assoc]
        rw [← congr($(hm a).left)]
        simp [fst_gluedCocone_ι_assoc]
      · 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
s : Cocone D
m : d.gluedCocone (P := P).pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
this :
  Iso.inv (d.pullbackGluedIso (P := P) i) ≫ CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) m =
    (d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)
refine_3 :
  𝒱.f i ≫ m.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    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))
⊢ 𝒱.f i ≫ m.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    𝒱.f i ≫
      CommaMorphism.left
        (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
          (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))

Tactic:
rw [Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left]

Premises used: AlgebraicGeometry.Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left
-- 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
m : d.gluedCocone (P := P).pt ⟶ s.pt
hm : ∀ (j : J), d.gluedCocone (P := P).ι.app j ≫ m = s.ι.app j
i : 𝒱.I₀
this :
  Iso.inv (d.pullbackGluedIso (P := P) i) ≫ CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) m =
    (d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)
⊢ 𝒱.f i ≫ m.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    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))

Tactic:
simp [𝒱, ← 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) 𝒰
H : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), P (trans (P := IsOpenImmersion) 𝒰 hij)
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 ⊤ (trans (P := IsOpenImmersion) 𝒰 hij))
inst_6 : ∀ (i : 𝒰.I₀), HasColimit (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i))
inst_7 : Quiver.IsThin.{u_2, v_2} 𝒰.I₀
inst_8 : Small.{u, u_2} 𝒰.I₀
inst_9 : IsZariskiLocalAtTarget P
⊢ HasColimit D

Tactic:
let d : ColimitGluingData D 𝒰 :=
    { cocone _ := colimit.cocone _
      isColimit _ := colimit.isColimit _
      prop_trans := H }
  ⟨d.gluedCocone, d.isColimitGluedCocone⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.Functor.comp, CategoryTheory.Limits.colimit.isColimit, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.mk, Nonempty.intro, CategoryTheory.Limits.HasColimit.mk', CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.MorphismProperty.Over.pullback, CategoryTheory.Limits.colimit.cocone, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone, Top.top, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimitGluedCocone
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
trans : {i j : 𝒰.I₀} → (hij : i ⟶ j) → 𝒰.X i ⟶ 𝒰.X j
trans_id : ∀ (i : 𝒰.I₀), trans (𝟙 i) = 𝟙 (𝒰.X i)
trans_comp : ∀ {i j k : 𝒰.I₀} (hij : i ⟶ j) (hjk : j ⟶ k), trans (hij ≫ hjk) = trans hij ≫ trans hjk
w : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), trans hij ≫ 𝒰.f j = 𝒰.f i
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
y : ↥(𝒰.X k)
⊢ trans hki ≫ 𝒰.f i = trans hkj ≫ 𝒰.f j

Tactic:
simp [w]
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{v_1, u, u_1} (P := P) 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
⊢ 𝒰.trans (P := P) hij ≫ 𝒰.f j = 𝒰.f i

Tactic:
LocallyDirected.w hij

Premises used: AlgebraicGeometry.Scheme.Cover.LocallyDirected.w
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{v_1, u, u_1} (P := P) 𝒰
i : 𝒰.I₀
⊢ trans.{v_1, u, u_1} (P := P) 𝒰 (𝟙 i) = 𝟙 (𝒰.X i)

Tactic:
LocallyDirected.trans_id i

Premises used: AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_id, AlgebraicGeometry.Scheme.Cover.trans
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{v_1, u, u_1} (P := P) 𝒰
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
⊢ 𝒰.trans (P := P) (hij ≫ hjk) = 𝒰.trans (P := P) hij ≫ 𝒰.trans (P := P) hjk

Tactic:
LocallyDirected.trans_comp hij hjk

Premises used: AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans_comp, AlgebraicGeometry.Scheme.Cover.trans
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{v_1, u, u_1} (P := P) 𝒰
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
k : 𝒰.I₀
hki : k ⟶ i
hkj : k ⟶ j
y : ↥(𝒰.X k)
⊢ 𝒰.trans (P := P) hki ≫ 𝒰.f i = 𝒰.trans (P := P) hkj ≫ 𝒰.f j

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{v_1, u, u_1} (P := P) 𝒰
i j : 𝒰.I₀
x : ↥(pullback (𝒰.f i) (𝒰.f j))
⊢ ∃ (k : 𝒰.I₀) (hki : k ⟶ i) (hkj : k ⟶ j) (y : ↥(𝒰.X k)),
    (pullback.lift (𝒰.trans (P := P) hki) (𝒰.trans (P := P) hkj) ⋯) y = x

Tactic:
LocallyDirected.directed x

Premises used: AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed, AlgebraicGeometry.Scheme.Cover.trans
-- Module: Mathlib.AlgebraicGeometry.Cover.Directed
Goal:
P : MorphismProperty Scheme
X : Scheme
𝒰 : Cover.{u_1, u} (precoverage P) X
inst : Category.{v_1, u_1} 𝒰.I₀
inst_1 : LocallyDirected.{v_1, u, u_1} (P := P) 𝒰
i j : 𝒰.I₀
xi : ↥(𝒰.X i)
xj : ↥(𝒰.X j)
h : Eq (α := ↥X) ((𝒰.f i) xi : ↥X) ((𝒰.f j) xj : ↥X)
obtain :
  ∀ (z : ↥(pullback (𝒰.f i) (𝒰.f j)))
    (h :
      Eq (α := ↥X) ((𝒰.f i) ((pullback.fst (𝒰.f i) (𝒰.f j)) z : ↥(𝒰.X i)) : ↥X)
        ((𝒰.f j) ((pullback.snd (𝒰.f i) (𝒰.f j)) z : ↥(𝒰.X j)) : ↥X)),
    ∃ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (xk : ↥(𝒰.X k)),
      Eq (α := ↥(𝒰.X i)) ((𝒰.trans (P := P) fi) xk : ↥(𝒰.X i)) ((pullback.fst (𝒰.f i) (𝒰.f j)) z : ↥(𝒰.X i)) ∧
        Eq (α := ↥(𝒰.X j)) ((𝒰.trans (P := P) fj) xk : ↥(𝒰.X j)) ((pullback.snd (𝒰.f i) (𝒰.f j)) z : ↥(𝒰.X j))
⊢ ∃ (k : 𝒰.I₀) (fi : k ⟶ i) (fj : k ⟶ j) (xk : ↥(𝒰.X k)), (𝒰.trans (P := P) fi) xk = xi ∧ (𝒰.trans (P := P) fj) xk = xj

Tactic:
obtain ⟨z, rfl, rfl⟩ := Scheme.Pullback.exists_preimage_pullback xi xj h

Premises used: AlgebraicGeometry.Scheme.Pullback.exists_preimage_pullback, rfl