-- 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₂
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)
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 ⋯ ⋯) ⟶
      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 ⋯ ⋯) ⟶
              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 ⋯ ⋯) ⟶
        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 ⋯ ⋯) ≫
        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 ⋯ ⋯) ⟶
        U)
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 ⋯ ⋯) ⟶
      V)
    (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 ⋯ ⋯) ⟶
              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.snd (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 ⋯ ⋯) ⟶
        V)
    (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.snd (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 ⋯ ⋯) ⟶
        V)
⊢ 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))

Tactic:
apply pullback.hom_ext

Premises used: CategoryTheory.Limits.pullback.hom_ext