awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
pf :
  Membership.mem (γ := Set X.Opens)
    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} f.domain
pf_1 : ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
H :
  ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap),
    g.domain =
      (↑(Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
            f.domain pf_1) :
        X.Opens)
pf_2 :
  H.choose (p := fun (g : X.PartialMap Y) ↦
        ∃ (_ : g.toRationalMap = f.toRationalMap),
          g.domain =
            (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                  Membership.mem (γ := Set X.Opens)
                    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                  f.domain pf_1) :
              X.Opens)).domain =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦
          Membership.mem (γ := Set X.Opens)
            {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
          f.domain pf) :
      X.Opens)
⊢ H.choose (p := fun (g : X.PartialMap Y) ↦
      ∃ (_ : g.toRationalMap = f.toRationalMap),
        g.domain =
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                Membership.mem (γ := Set X.Opens)
                  {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                f.domain pf_1) :
            X.Opens)) =
    f

Tactic:
have : H.choose = f := (equiv_iff_of_domain_eq_of_isSeparated (S := ⊤_ _) H.choose_spec.2).mp
    (toRationalMap_eq_iff.mp H.choose_spec.1)
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
pf :
  Membership.mem (γ := Set X.Opens)
    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} f.domain
pf_1 : ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
H :
  ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap),
    g.domain =
      (↑(Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
            f.domain pf_1) :
        X.Opens)
pf_2 :
  H.choose (p := fun (g : X.PartialMap Y) ↦
        ∃ (_ : g.toRationalMap = f.toRationalMap),
          g.domain =
            (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                  Membership.mem (γ := Set X.Opens)
                    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                  f.domain pf_1) :
              X.Opens)).domain =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦
          Membership.mem (γ := Set X.Opens)
            {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
          f.domain pf) :
      X.Opens)
this :
  H.choose (p := fun (g : X.PartialMap Y) ↦
      ∃ (_ : g.toRationalMap = f.toRationalMap),
        g.domain =
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                Membership.mem (γ := Set X.Opens)
                  {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                f.domain pf_1) :
            X.Opens)) =
    f
⊢ (X.isoOfEq pf_2).inv ≫
      H.choose (p := fun (g : X.PartialMap Y) ↦
          ∃ (_ : g.toRationalMap = f.toRationalMap),
            g.domain =
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                    Membership.mem (γ := Set X.Opens)
                      {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                    f.domain pf_1) :
                X.Opens)).hom =
    f.hom

Tactic:
((ext_iff _ _).mp this.symm).choose_spec.symm

Premises used: AlgebraicGeometry.Scheme.PartialMap.ext_iff, Exists.choose_spec, Set.Mem, AlgebraicGeometry.Scheme.restrict, Iff.mp, Eq.symm, AlgebraicGeometry.Scheme.Opens.toScheme
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
pf :
  Membership.mem (γ := Set X.Opens)
    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} f.domain
pf_1 : ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = f.domain
H :
  ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap),
    g.domain =
      (↑(Subtype.mk (p := fun (x : X.Opens) ↦
            Membership.mem (γ := Set X.Opens)
              {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
            f.domain pf_1) :
        X.Opens)
pf_2 :
  H.choose (p := fun (g : X.PartialMap Y) ↦
        ∃ (_ : g.toRationalMap = f.toRationalMap),
          g.domain =
            (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                  Membership.mem (γ := Set X.Opens)
                    {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                  f.domain pf_1) :
              X.Opens)).domain =
    (↑(Subtype.mk (p := fun (x : X.Opens) ↦
          Membership.mem (γ := Set X.Opens)
            {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
          f.domain pf) :
      X.Opens)
this :
  H.choose (p := fun (g : X.PartialMap Y) ↦
      ∃ (_ : g.toRationalMap = f.toRationalMap),
        g.domain =
          (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                Membership.mem (γ := Set X.Opens)
                  {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                f.domain pf_1) :
            X.Opens)) =
    f
⊢ (X.isoOfEq pf_2).inv ≫
      H.choose (p := fun (g : X.PartialMap Y) ↦
          ∃ (_ : g.toRationalMap = f.toRationalMap),
            g.domain =
              (↑(Subtype.mk (p := fun (x : X.Opens) ↦
                    Membership.mem (γ := Set X.Opens)
                      {x : X.Opens | ∃ (g : X.PartialMap Y) (_ : g.toRationalMap = f.toRationalMap), g.domain = x} x)
                    f.domain pf_1) :
                X.Opens)).hom =
    f.hom

Tactic:
exact ((ext_iff _ _).mp this.symm).choose_spec.symm

Premises used: AlgebraicGeometry.Scheme.PartialMap.ext_iff, Exists.choose_spec, Iff.mp, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X ⤏ Y
obtain : ∀ (f : X.PartialMap Y), f.toRationalMap.toPartialMap.toRationalMap = f.toRationalMap
⊢ f.toPartialMap.toRationalMap = f

Tactic:
obtain ⟨f, rfl⟩ := PartialMap.toRationalMap_surjective f

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
trans : f.toRationalMap.toPartialMap.toRationalMap = (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap
trans₁ : (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap = f.toRationalMap
⊢ f.toRationalMap.toPartialMap.toRationalMap = f.toRationalMap

Tactic:
trans (f.toRationalMap.toPartialMap.restrict _
    f.dense_domain f.le_domain_toRationalMap).toRationalMap

Premises used: AlgebraicGeometry.Scheme.PartialMap.toRationalMap, AlgebraicGeometry.Scheme.RationalMap.toPartialMap, AlgebraicGeometry.Scheme.PartialMap.restrict, AlgebraicGeometry.Scheme.PartialMap.dense_domain, AlgebraicGeometry.Scheme.PartialMap.le_domain_toRationalMap
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.toRationalMap = (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
e_f : f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯ = f
⊢ (f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯).toRationalMap = f.toRationalMap

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y : Scheme
inst : IsReduced X
inst_1 : Y.IsSeparated
f : X.PartialMap Y
⊢ f.toRationalMap.toPartialMap.restrict f.domain ⋯ ⋯ = f

Tactic:
exact PartialMap.ext _ f rfl (by simpa using f.toPartialMap_toRationalMap_restrict)

Premises used: AlgebraicGeometry.Scheme.PartialMap.ext, rfl
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
inst_2 : S.IsSeparated
inst_3 : X.Over S
inst_4 : Y.Over S
f : X ⤏ Y
inst_5 rw : RationalMap.IsOver S f
⊢ PartialMap.IsOver S f.toPartialMap

Tactic:
rw [← PartialMap.isOver_toRationalMap_iff_of_isSeparated, f.toRationalMap_toPartialMap]

Premises used: AlgebraicGeometry.Scheme.RationalMap.toRationalMap_toPartialMap, AlgebraicGeometry.Scheme.PartialMap.isOver_toRationalMap_iff_of_isSeparated
-- Module: Mathlib.AlgebraicGeometry.Birational.RationalMap
Goal:
X Y Z S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : IsReduced X
inst_1 : Y.IsSeparated
inst_2 : S.IsSeparated
inst_3 : X.Over S
inst_4 : Y.Over S
f : X ⤏ Y
inst_5 : RationalMap.IsOver S f
⊢ RationalMap.IsOver S f

Tactic:
infer_instance
-- 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 𝒰
i j : 𝒰.I₀
hij : i ⟶ j
a : J
⊢ Eq (α :=
    Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).obj a) ⟶
      (d.cocone (P := P) j).pt)
    (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) ((d.cocone (P := P) i).ι.app a) ≫
        d.transitionMap (P := P) hij :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)).obj a) ⟶
        (d.cocone (P := P) j).pt)
    (NatTrans.app (d.trans (P := P) hij) a ≫ (d.cocone (P := P) j).ι.app a :
      (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj a ⟶
        Functor.obj.{v_1, u, u_1, u + 1} (Functor.obj (Functor.const J) (d.cocone (P := P) j).pt) a)

Tactic:
simp [transitionMap, ← Functor.mapCocone_ι_app, transitionCocone]

Premises used: CategoryTheory.Functor.mapCocone_ι_app, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionMap, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.transitionCocone
-- 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 𝒰
i : 𝒰.I₀
apply :
  ∀ (j : J),
    Eq (α :=
      ((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j ⟶
        (d.cocone (P := P) i).pt)
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, u, u_1, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
              (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
          j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))) j)
        (d.transitionMap (P := P) (𝟙 i)))
      (CategoryStruct.comp (Y :=
        Functor.obj.{v_1, u, u_1, u + 1}
          (Functor.obj (Functor.const J)
            (Cocone.pt (F := (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
              (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
          j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))) j)
        (NatTrans.app
          (Iso.hom
            (MorphismProperty.Over.mapId (P := P) ⊤ (𝒰.X i) (Cover.trans.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰 (𝟙 i))
              ⋯))
          (d.cocone (P := P) i).pt))
⊢ Eq (α := Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) i).pt)
    (d.transitionMap (P := P) (𝟙 i) :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶ (d.cocone (P := P) i).pt)
    (NatTrans.app
        (Iso.hom
          (MorphismProperty.Over.mapId (P := P) ⊤ (𝒰.X i) (Cover.trans.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰 (𝟙 i)) ⋯))
        (d.cocone (P := P) i).pt :
      Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt ⟶
        Functor.obj (𝟭 (P.Over ⊤ (𝒰.X i))) (d.cocone (P := P) i).pt)

Tactic:
apply (isColimitOfPreserves (Over.map ⊤ (d.prop_trans <| 𝟙 i)) (d.isColimit i)).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.MorphismProperty.Over.map, CategoryTheory.CategoryStruct.id, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.prop_trans, Top.top, AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimit, CategoryTheory.Limits.isColimitOfPreserves
-- 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 𝒰
i : 𝒰.I₀
j : J
⊢ Eq (α :=
    (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j).toComma (P := P)
          (Q := ⊤) (W := ⊤).left ⟶
      (d.cocone (P := P) i).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, u, u_1, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F :=
                (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
            j)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))) j)
          (d.transitionMap (P := P) (𝟙 i)))))
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, u, u_1, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F :=
                (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
            j)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))) j)
          (NatTrans.app
            (Iso.hom
              (MorphismProperty.Over.mapId (P := P) ⊤ (𝒰.X i) (Cover.trans.{v_2, u, u_2} (P := IsOpenImmersion) 𝒰 (𝟙 i))
                ⋯))
            (d.cocone (P := P) i).pt))))

Tactic:
simp [cocone_ι_transitionMap]

Premises used: AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap
-- 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 𝒰
i j k : 𝒰.I₀
hij : i ⟶ j
hjk : j ⟶ k
j_1 : J
⊢ Eq (α :=
    (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯).obj j_1).toComma (P :=
          P) (Q := ⊤) (W := ⊤).left ⟶
      (d.cocone (P := P) k).pt.toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, u, u_1, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F :=
                (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
            j_1)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i)))
            j_1)
          (d.transitionMap (P := P) (hij ≫ hjk)))))
    (CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (CategoryStruct.comp (Y :=
          Functor.obj.{v_1, u, u_1, u + 1}
            (Functor.obj (Functor.const J)
              (Cocone.pt (F :=
                (D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ ⋯)
                (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i))))
            j_1)
          (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i)))
            j_1)
          (NatTrans.app
              (Iso.hom
                (MorphismProperty.Over.mapComp (P := P) ⊤ ⋯ ⋯ (Cover.trans (P := IsOpenImmersion) 𝒰 (hij ≫ hjk)) ⋯))
              (d.cocone (P := P) i).pt ≫
            CategoryStruct.comp (Y := Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt)
              (CategoryTheory.Functor.map (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.transitionMap (P := P) hij) :
                Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯)
                    (Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) i).pt) ⟶
                  Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt)
              (d.transitionMap (P := P) hjk :
                Functor.obj (MorphismProperty.Over.map (P := P) ⊤ ⋯) (d.cocone (P := P) j).pt ⟶
                  (d.cocone (P := P) k).pt)))))

Tactic:
simp [← Functor.map_comp_assoc, cocone_ι_transitionMap, pullback.map_comp_assoc]

Premises used: AlgebraicGeometry.Scheme.Cover.ColimitGluingData.cocone_ι_transitionMap, CategoryTheory.Limits.pullback.map_comp_assoc, CategoryTheory.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))
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) ⟶
      (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).left)
    (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.fst (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.fst (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))

Tactic:
simp