-- Mathlib/AlgebraicGeometry/Morphisms/Constructors.lean
theorem HasAffineProperty.diagonal_of_openCover (P) {Q} [HasAffineProperty P Q]
    {X Y : Scheme.{u}} (f : X ⟶ Y) (𝒰 : Scheme.OpenCover.{u} Y) [∀ i, IsAffine (𝒰.obj i)]
    (𝒰' : ∀ i, Scheme.OpenCover.{u} (pullback f (𝒰.map i))) [∀ i j, IsAffine ((𝒰' i).obj j)]
    (h𝒰' : ∀ i j k,
      Q (pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (𝒰.pullbackHom f i))) :
    P.diagonal f

Proof state:
case mk.mk.convert_2
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
𝒰' : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝ : ∀ (i : 𝒰.J) (j : (𝒰' i).J), IsAffine ((𝒰' i).obj j)
h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : Scheme.Cover (@IsOpenImmersion) (pullback f f) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))
i1 : ∀ (i : 𝒱.J), IsAffine (𝒱.obj i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).J
j k : (𝒰' i).J
⊢ pullback.map ((𝒰' i).map j ≫ pullback.snd f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.snd f (𝒰.map i)) f f
        ((𝒰' i).map j ≫ pullback.fst f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.fst f (𝒰.map i)) (𝒰.map i) ⋯ ⋯ ≫
      𝟙 (pullback.diagonalObj f) =
    𝟙 (pullback ((𝒰' i).map j ≫ pullback.snd f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.snd f (𝒰.map i))) ≫
      pullback.map ((𝒰' i).map j ≫ pullback.snd f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.snd f (𝒰.map i))
          (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i)) ((𝒰' i).map j) ((𝒰' i).map k) (𝟙 (𝒰.obj i)) ⋯ ⋯ ≫
        pullback.map (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i)) f f (pullback.fst f (𝒰.map i))
          (pullback.fst f (𝒰.map i)) (𝒰.map i) ⋯ ⋯

Tactic:
ext1 <;> simp

Result:
no goals

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
𝒰' : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝ : ∀ (i : 𝒰.J) (j : (𝒰' i).J), IsAffine ((𝒰' i).obj j)
h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : Scheme.Cover (@IsOpenImmersion) (pullback f f) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))
⊢ P.diagonal f

Tactic:
have i1 : ∀ i, IsAffine (𝒱.obj i) := fun i => by dsimp [𝒱]; infer_instance

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
𝒰' : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝ : ∀ (i : 𝒰.J) (j : (𝒰' i).J), IsAffine ((𝒰' i).obj j)
h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : Scheme.Cover (@IsOpenImmersion) (pullback f f) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))
i1 : ∀ (i : 𝒱.J), IsAffine (𝒱.obj i)
⊢ P.diagonal f

Proof state:
case mk.mk.convert_6
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
𝒰' : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝ : ∀ (i : 𝒰.J) (j : (𝒰' i).J), IsAffine ((𝒰' i).obj j)
h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : Scheme.Cover (@IsOpenImmersion) (pullback f f) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))
i1 : ∀ (i : 𝒱.J), IsAffine (𝒱.obj i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).J
j k : (𝒰' i).J
⊢ Q
    ((pullbackDiagonalMapIso f (𝒰.map i) ((𝒰' i).map j) ((𝒰' i).map k)).inv ≫
      pullback.snd (pullback.diagonal f)
        (pullback.map ((𝒰' i).map j ≫ pullback.snd f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.snd f (𝒰.map i)) f f
          ((𝒰' i).map j ≫ pullback.fst f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.fst f (𝒰.map i)) (𝒰.map i) ⋯ ⋯))

Tactic:
convert h𝒰' i j k

Result:
case h.e'_3.h
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
𝒰' : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝ : ∀ (i : 𝒰.J) (j : (𝒰' i).J), IsAffine ((𝒰' i).obj j)
h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : Scheme.Cover (@IsOpenImmersion) (pullback f f) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))
i1 : ∀ (i : 𝒱.J), IsAffine (𝒱.obj i)
i : (Scheme.Pullback.openCoverOfBase 𝒰 f f).J
j k : (𝒰' i).J
e_2✝ :
  pullback ((𝒰' i).map j ≫ pullback.snd f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.snd f (𝒰.map i)) =
    pullback ((𝒰' i).map j ≫ Scheme.Cover.pullbackHom 𝒰 f i) ((𝒰' i).map k ≫ Scheme.Cover.pullbackHom 𝒰 f i)
⊢ (pullbackDiagonalMapIso f (𝒰.map i) ((𝒰' i).map j) ((𝒰' i).map k)).inv ≫
      pullback.snd (pullback.diagonal f)
        (pullback.map ((𝒰' i).map j ≫ pullback.snd f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.snd f (𝒰.map i)) f f
          ((𝒰' i).map j ≫ pullback.fst f (𝒰.map i)) ((𝒰' i).map k ≫ pullback.fst f (𝒰.map i)) (𝒰.map i) ⋯ ⋯) =
    pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i)

Proof state:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
𝒰' : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝ : ∀ (i : 𝒰.J) (j : (𝒰' i).J), IsAffine ((𝒰' i).obj j)
h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : Scheme.Cover (@IsOpenImmersion) (pullback f f) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))
i : 𝒱.J
⊢ IsAffine (𝒱.obj i)

Tactic:
dsimp [𝒱]

Result:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝² : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
𝒰 : Y.OpenCover
inst✝¹ : ∀ (i : 𝒰.J), IsAffine (𝒰.obj i)
𝒰' : (i : 𝒰.J) → (pullback f (𝒰.map i)).OpenCover
inst✝ : ∀ (i : 𝒰.J) (j : (𝒰' i).J), IsAffine ((𝒰' i).obj j)
h𝒰' : ∀ (i : 𝒰.J) (j k : (𝒰' i).J), Q (pullback.mapDesc ((𝒰' i).map j) ((𝒰' i).map k) (Scheme.Cover.pullbackHom 𝒰 f i))
this : Q.IsLocal := isLocal_affineProperty P
𝒱 : Scheme.Cover (@IsOpenImmersion) (pullback f f) :=
  Scheme.Cover.bind (Scheme.Pullback.openCoverOfBase 𝒰 f f) fun i =>
    Scheme.Pullback.openCoverOfLeftRight (𝒰' i) (𝒰' i) (pullback.snd f (𝒰.map i)) (pullback.snd f (𝒰.map i))
i : 𝒱.J
⊢ IsAffine
    (pullback ((𝒰' i.fst).map i.snd.1 ≫ pullback.snd f (𝒰.map i.fst))
      ((𝒰' i.fst).map i.snd.2 ≫ pullback.snd f (𝒰.map i.fst)))