-- 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))
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
h :
  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)))
⊢ Eq (α :=
    pullback (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f i) ⟶
      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.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) ⋯ ⋯)
have h₁ : 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) sorry sorry ≫
        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) sorry sorry)
    (pullback.snd (D.obj a).toComma (P := P) (Q := ⊤) (W := ⊤).hom (𝒰.f j)))
Tactic: apply pullback.hom_ext