-- Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors
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₂
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 ⋯ ⋯) =
      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 (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))
convert_1 : IsAffine.{u} (pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g))
convert_2 :
  IsOpenImmersion (X := pullback (f₁ ≫ pullback.snd f g) (f₂ ≫ pullback.snd f g)) (Y := pullback.diagonalObj 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
      ⋯ ⋯)
⊢ 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))

Tactic:
convert! HasAffineProperty.of_isPullback (P := P) (.of_hasPullback _ _) H

Premises used: AlgebraicGeometry.HasAffineProperty.of_isPullback, CategoryTheory.IsPullback.of_hasPullback