-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Constructors (goal)
Goal:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst : HasAffineProperty P Q
X Y U_1 V_1 : Scheme
f : X ⟶ Y
g : U_1 ⟶ Y
inst_1 : IsAffine U_1
inst_2 : IsOpenImmersion g
iV : V_1 ⟶ X
f' : V_1 ⟶ U_1
h : IsPullback iV f' f g
H : P.diagonal f
this : Q.IsLocal := ⋯
U V : Scheme
f₁ : U ⟶ pullback f g
f₂ : V ⟶ pullback f g
hU : IsAffine U
hV : IsAffine V
hf₁ : IsOpenImmersion f₁
hf₂ : IsOpenImmersion f₂
e_1 :
  pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯) =
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g ⋯ ⋯)
e_2 :
  pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) = pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)
⊢ Eq (α :=
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
        (pullback.diagonal f)
        (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
          (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
      pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
    (CategoryStruct.comp (Y := pullback f₁ f₂)
        (Iso.hom (pullbackDiagonalMapIso f g f₁ f₂) :
          pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
              (pullback.diagonal f)
              (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
                (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
            pullback f₁ f₂)
        (pullback.mapDesc f₁ f₂ (pullback.snd f g) :
          pullback f₁ f₂ ⟶ pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) :
      pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
          (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
        pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
    (pullback.snd (pullback.diagonal f)
        (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
          (f₂ ≫ pullback.fst f g) g ⋯ ⋯) :
      pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
          (pullback.diagonal f)
          (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
            (f₂ ≫ pullback.fst f g) g ⋯ ⋯) ⟶
        pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
have h₁ : Eq (α :=
  pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
      (pullback.diagonal f)
      (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g) (f₂ ≫ pullback.fst f g)
        g sorry sorry) ⟶
    U)
  (CategoryStruct.comp (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
      (CategoryStruct.comp (Y := pullback f₁ f₂)
        (Iso.hom (pullbackDiagonalMapIso f g f₁ f₂) :
          pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
              (pullback.diagonal f)
              (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
                (f₂ ≫ pullback.fst f g) g sorry sorry) ⟶
            pullback f₁ f₂)
        (pullback.mapDesc f₁ f₂ (pullback.snd f g) :
          pullback f₁ f₂ ⟶ pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)))
      (pullback.fst (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) :
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
        (pullback.diagonal f)
        (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
          (f₂ ≫ pullback.fst f g) g sorry sorry) ⟶
      U)
  (pullback.snd (pullback.diagonal f)
        (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
          (f₂ ≫ pullback.fst f g) g sorry sorry) ≫
      pullback.fst (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) :
    pullback (Y := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Z := pullback.diagonalObj f)
        (pullback.diagonal f)
        (pullback.map (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g) f f (f₁ ≫ pullback.fst f g)
          (f₂ ≫ pullback.fst f g) g sorry sorry) ⟶
      U)
Tactic: apply pullback.hom_ext