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))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone (P := P) i).pt ≅
  Cocone.pt (F :=
    (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) ⋙
      MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
    (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.cocone (P := P) j)) :=
  (d.isColimit (P := P) i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.isColimit (P := P) j))
    (D.isoWhiskerLeft
        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝒰.f j) (𝒰.f i)
          ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm)
a : J
⊢ Eq (α := pullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ⟶ 𝒰.X j)
    (CategoryStruct.comp (Y := pullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
      (CategoryStruct.comp (Y :=
        pullback (X := pullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
          (pullback.snd (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
          (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
        (pullback.map (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)
            (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫ 𝒰.f j)
            (𝟙 (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).left) (𝟙 (𝒰.X i)) (𝟙 S) ⋯ ⋯ ≫
          Iso.inv
            (pullbackLeftPullbackSndIso (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)
              (Cover.trans (P := IsOpenImmersion) 𝒰 hij)))
        (pullback.fst (pullback.snd (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
          (Cover.trans (P := IsOpenImmersion) 𝒰 hij)))
      (pullback.snd (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))
    (CategoryStruct.comp (Y := pullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j))
      (pullback.map (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i)
        (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j) (𝟙 (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).left)
        (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝟙 S) ⋯ ⋯)
      (pullback.snd (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))

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))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone (P := P) i).pt ≅
  Cocone.pt (F :=
    (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) ⋙
      MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
    (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.cocone (P := P) j)) :=
  (d.isColimit (P := P) i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.isColimit (P := P) j))
    (D.isoWhiskerLeft
        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝒰.f j) (𝒰.f i)
          ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm)
⊢ Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
      Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) iso1.hom ≫
        NatTrans.app
          (Adjunction.counit
            (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial))
          (d.cocone (P := P) j).pt :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (d.transitionMap (P := P) hij :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) j).pt)

Tactic:
have heq : (Over.map _ (d.prop_trans hij)).map iso1.hom ≫
        (Over.mapPullbackAdj _ _ _ (d.prop_trans hij) trivial).counit.app _ =
      d.transitionMap hij := by
    apply (isColimitOfPreserves (Over.map _ (d.prop_trans hij)) (d.isColimit i)).hom_ext
    intro a
    dsimp only [Functor.comp_obj, Functor.id_obj, Functor.mapCocone_pt, Functor.const_obj_obj,
      Functor.mapCocone_ι_app, Iso.trans_hom, Functor.isoWhiskerLeft_hom, Iso.symm_hom]
    rw [IsColimit.coconePointsIsoOfNatIso_hom, ← Functor.map_comp_assoc, IsColimit.ι_map,
      Functor.mapCocone_ι_app, Functor.map_comp, Category.assoc,
      Adjunction.counit_naturality, cocone_ι_transitionMap]
    ext
    dsimp
    rw [Category.comp_id, ← Category.assoc]
    congr 1
    apply pullback.hom_ext <;> 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))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone (P := P) i).pt ≅
  Cocone.pt (F :=
    (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) ⋙
      MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
    (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.cocone (P := P) j)) :=
  (d.isColimit (P := P) i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.isColimit (P := P) j))
    (D.isoWhiskerLeft
        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝒰.f j) (𝒰.f i)
          ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm)
heq :
  Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
      Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) iso1.hom ≫
        NatTrans.app
          (Adjunction.counit
            (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial))
          (d.cocone (P := P) j).pt :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (d.transitionMap (P := P) hij :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) j).pt)
iso2 : (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  pullback (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (Cover.trans (P := IsOpenImmersion) 𝒰 hij) :=
  Functor.mapIso (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)) iso1
⊢ (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom ≫
      Iso.hom
        (Iso.refl
          (Functor.obj (Functor.fromPUnit (𝒰.X j)) (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).right)) =
    Iso.hom (Iso.refl (Functor.obj (𝟭 Scheme) (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)) ≫
      (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom

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))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone (P := P) i).pt ≅
  Cocone.pt (F :=
    (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) ⋙
      MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
    (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.cocone (P := P) j)) :=
  (d.isColimit (P := P) i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.isColimit (P := P) j))
    (D.isoWhiskerLeft
        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝒰.f j) (𝒰.f i)
          ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm)
heq :
  Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
      Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) iso1.hom ≫
        NatTrans.app
          (Adjunction.counit
            (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial))
          (d.cocone (P := P) j).pt :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (d.transitionMap (P := P) hij :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) j).pt)
iso2 : (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  pullback (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (Cover.trans (P := IsOpenImmersion) 𝒰 hij) :=
  Functor.mapIso (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)) iso1
⊢ Cover.trans (P := IsOpenImmersion) 𝒰 hij ≫
      Iso.hom
        (Iso.refl
          (Functor.obj (Functor.fromPUnit (𝒰.X j)) (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).right)) =
    Iso.hom (Iso.refl (𝒰.X i)) ≫ Cover.trans (P := IsOpenImmersion) 𝒰 hij

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))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone (P := P) i).pt ≅
  Cocone.pt (F :=
    (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) ⋙
      MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
    (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.cocone (P := P) j)) :=
  (d.isColimit (P := P) i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.isColimit (P := P) j))
    (D.isoWhiskerLeft
        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝒰.f j) (𝒰.f i)
          ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm)
heq :
  Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
      Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) iso1.hom ≫
        NatTrans.app
          (Adjunction.counit
            (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial))
          (d.cocone (P := P) j).pt :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (d.transitionMap (P := P) hij :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) j).pt)
iso2 : (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  pullback (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (Cover.trans (P := IsOpenImmersion) 𝒰 hij) :=
  Functor.mapIso (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)) iso1
⊢ pullback.fst (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom
        (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ≫
      Iso.hom (Iso.refl (Functor.obj (𝟭 Scheme) (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)) =
    iso2.symm.hom ≫
      CommaMorphism.left (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤) (d.transitionMap (P := P) hij))

Tactic:
simpa [← cancel_epi iso2.hom] using congr($(heq).left)

Premises used: CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- 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))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone (P := P) i).pt ≅
  Cocone.pt (F :=
    (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) ⋙
      MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
    (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.cocone (P := P) j)) :=
  (d.isColimit (P := P) i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.isColimit (P := P) j))
    (D.isoWhiskerLeft
        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝒰.f j) (𝒰.f i)
          ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm)
heq :
  Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
      Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) iso1.hom ≫
        NatTrans.app
          (Adjunction.counit
            (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial))
          (d.cocone (P := P) j).pt :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (d.transitionMap (P := P) hij :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) j).pt)
iso2 : (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  pullback (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (Cover.trans (P := IsOpenImmersion) 𝒰 hij) :=
  Functor.mapIso (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)) iso1
⊢ pullback.snd (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom
        (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ≫
      Iso.hom (Iso.refl (𝒰.X i)) =
    iso2.symm.hom ≫ (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom

Tactic:
(Over.w iso1.inv).symm

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.NatTrans.vcomp, Set.Mem, setOf, ContinuousMap.comp, CategoryTheory.Limits.limit, Set.preimage, AlgebraicGeometry.PresheafedSpace.comp, CategoryTheory.MorphismProperty.Over.w, AlgebraicGeometry.LocallyRingedSpace.comp, Eq.symm, CategoryTheory.Iso.inv
-- 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))
i j : 𝒰.I₀
hij : i ⟶ j
iso1 : (d.cocone (P := P) i).pt ≅
  Cocone.pt (F :=
    (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f j)) ⋙
      MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
    (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.cocone (P := P) j)) :=
  (d.isColimit (P := P) i).coconePointsIsoOfNatIso
    (isColimitOfPreserves (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))
      (d.isColimit (P := P) j))
    (D.isoWhiskerLeft
        (MorphismProperty.Over.pullbackComp (P := P) (Q := ⊤) (Cover.trans (P := IsOpenImmersion) 𝒰 hij) (𝒰.f j) (𝒰.f i)
          ⋯) ≪≫
      (D.associator (MorphismProperty.Over.pullback P ⊤ (𝒰.f j))
          (MorphismProperty.Over.pullback P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij))).symm)
heq :
  Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
      Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) iso1.hom ≫
        NatTrans.app
          (Adjunction.counit
            (MorphismProperty.Over.mapPullbackAdj P ⊤ (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ⋯ trivial))
          (d.cocone (P := P) j).pt :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (𝟭 (P.Over ⊤ (𝒰.X j))) (d.cocone (P := P) j).pt)
    (d.transitionMap (P := P) hij :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) j).pt)
iso2 : (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left ≅
  pullback (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (Cover.trans (P := IsOpenImmersion) 𝒰 hij) :=
  Functor.mapIso (MorphismProperty.Over.forget P ⊤ (𝒰.X i) ⋙ CategoryTheory.Over.forget (𝒰.X i)) iso1
⊢ pullback.snd (d.cocone (P := P) j).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom
        (Cover.trans (P := IsOpenImmersion) 𝒰 hij) ≫
      Iso.hom (Iso.refl (𝒰.X i)) =
    iso2.symm.hom ≫ (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom

Tactic:
exact (Over.w iso1.inv).symm

Premises used: CategoryTheory.MorphismProperty.Over.w, Eq.symm, CategoryTheory.Iso.inv
-- 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
rw :
  ∀ (i : 𝒰.toPreZeroHypercover.1),
    P (X :=
      PreZeroHypercover.X
        (Precoverage.ZeroHypercover.toPreZeroHypercover
          (Precoverage.ZeroHypercover.pullback₁ d.relativeGluingData (P := P).toBase 𝒰))
        i)
      (pullbackHom (P := IsOpenImmersion) 𝒰 d.relativeGluingData (P := P).toBase i :
        PreZeroHypercover.X
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (Precoverage.ZeroHypercover.pullback₁ d.relativeGluingData (P := P).toBase 𝒰))
            i ⟶
          𝒰.X i)
⊢ P (X := d.relativeGluingData (P := P).glued) d.relativeGluingData (P := P).toBase

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := P) 𝒰]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover