-- 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 𝒰
i : 𝒰.I₀
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))
have h : Eq (α :=
  (((D ⋙ MorphismProperty.Over.pullback P ⊤ (𝒰.f i)) ⋙ MorphismProperty.Over.map (P := P) ⊤ sorry).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) ⊤ sorry)
              (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i))))
          j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ sorry) (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) ⊤ sorry)
              (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ sorry) (d.cocone (P := P) i))))
          j)
        (NatTrans.app (Cocone.ι (Functor.mapCocone (MorphismProperty.Over.map (P := P) ⊤ sorry) (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))
              sorry))
          (d.cocone (P := P) i).pt))))
Tactic: ext