awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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
⊢ m.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left =
    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))
have refine_3 : ∀ (i : 𝒱.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)))
              sorry sorry)
            trivial trivial))
Tactic: refine 𝒱.hom_ext _ _ fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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)
have refine : ∀ (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 =
    (d.cocone (P := P) i).ι.app a ≫
      (d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)
Tactic: refine (d.isColimit i).hom_ext fun a ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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 =
    (d.cocone (P := P) i).ι.app a ≫
      (d.isColimit (P := P) i).desc (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)
have rw : (d.cocone (P := P) i).ι.app a ≫
    Iso.inv (d.pullbackGluedIso (P := P) i) ≫
      CategoryTheory.Functor.map (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) m =
  NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)) a
Tactic: rw [IsColimit.fac]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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 =
    NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)) a
have h : ((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 =
  CommaMorphism.left
    (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
      (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)) a))
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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 =
    CommaMorphism.left
      (Comma.Hom.toCommaMorphism (P := P) (Q := ⊤) (W := ⊤)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) s)) a))
have h : ((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: apply pullback.hom_ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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.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)
have 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)) sorry)
    (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)) sorry)
    (pullback.fst s.pt.toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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
⊢ 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))
have 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
Tactic: simp only [Category.assoc, limit.lift_π, PullbackCone.mk_π_app,
          pullbackGluedIso_inv_fst_assoc]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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) ≫
      (s.ι.app a).toCommaMorphism (P := P) (Q := ⊤) (W := ⊤).left
have 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
Tactic: rw [← congr($(hm a).left)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (hypothesis)
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₀
⊢ 𝒱.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))
have 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)
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.ColimitsOver (goal)
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 =
    𝒱.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))
have 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))
Tactic: rw [Scheme.OpenCover.map_glueMorphismsOverOfLocallyDirected_left]