-- 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:
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
⊢ P.diagonal f

Tactic:
let 𝒱 := (Scheme.Pullback.openCoverOfBase 𝒰 f f).bind fun i =>
  Scheme.Pullback.openCoverOfLeftRight.{u} (𝒰' i) (𝒰' i) (pullback.snd _ _) (pullback.snd _ _)

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))
⊢ P.diagonal f

Proof state:
case mk.mk.convert_1
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.diagonal f ≫ 𝟙 (pullback.diagonalObj f) = 𝟙 X ≫ pullback.diagonal f

Tactic:
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))
⊢ P.diagonal f

Tactic:
letI := isLocal_affineProperty P

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
⊢ P.diagonal f

Proof state:
case mk.mk
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 (𝒱.pullbackHom (pullback.diagonal f) ⟨i, (j, k)⟩)

Tactic:
dsimp [𝒱]

Result:
case mk.mk
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
    ((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))).pullbackHom
      (pullback.diagonal f) ⟨i, (j, k)⟩)

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
    (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)))

Tactic:
infer_instance

Result:
no goals