-- 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₂
⊢ Q (X :=
    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 ⋯ ⋯))
    (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 ⋯ ⋯) ⟶
            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))
have h₁ : 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 (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₁ ≫ 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 sorry sorry) ⟶
        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 (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₁ ≫ 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 sorry sorry) :
        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₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
Tactic: convert! HasAffineProperty.of_isPullback (P := P) (.of_hasPullback _ _) H