-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem quasiCompact_affineProperty_iff_quasiSeparatedSpace {X Y : Scheme} [IsAffine Y]
    (f : X ⟶ Y) :
    AffineTargetMorphismProperty.diagonal (fun X _ _ _ ↦ CompactSpace X) f ↔
      QuasiSeparatedSpace X

Proof state:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
    [inst_2 : IsOpenImmersion f₁] [inst_3 : IsOpenImmersion f₂],
    (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f))
      (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
haveI : IsAffine _ := U.2

Result:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
    [inst_2 : IsOpenImmersion f₁] [inst_3 : IsOpenImmersion f₂],
    (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f))
      (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
this : IsAffine ↑↑U
⊢ IsCompact (↑↑U ∩ ↑↑V)

Proof state:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
    [inst_2 : IsOpenImmersion f₁] [inst_3 : IsOpenImmersion f₂],
    (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f))
      (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
this✝¹ : IsAffine ↑↑U
this✝ : IsAffine ↑↑V
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
this : IsOpenImmersion g
e : ↑↑(pullback (↑U).ι (↑V).ι).toPresheafedSpace ≃ₜ ↑(Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom g).base))
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
rw [IsOpenImmersion.range_pullback_to_base_of_left] at e

Result:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
    [inst_2 : IsOpenImmersion f₁] [inst_3 : IsOpenImmersion f₂],
    (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f))
      (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
this✝¹ : IsAffine ↑↑U
this✝ : IsAffine ↑↑V
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
this : IsOpenImmersion g
e :
  ↑↑(pullback (↑U).ι (↑V).ι).toPresheafedSpace ≃ₜ
    ↑(Set.range ⇑(ConcreteCategory.hom (↑U).ι.base) ∩ Set.range ⇑(ConcreteCategory.hom (↑V).ι.base))
⊢ IsCompact (↑↑U ∩ ↑↑V)

Proof state:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
    [inst_2 : IsOpenImmersion f₁] [inst_3 : IsOpenImmersion f₂],
    (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f))
      (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
this✝¹ : IsAffine ↑↑U
this✝ : IsAffine ↑↑V
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
this : IsOpenImmersion g
e :
  ↑↑(pullback (↑U).ι (↑V).ι).toPresheafedSpace ≃ₜ
    ↑(Set.range ⇑(ConcreteCategory.hom (↑U).ι.base) ∩ Set.range ⇑(ConcreteCategory.hom (↑V).ι.base))
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
erw [Subtype.range_coe, Subtype.range_coe] at e

Result:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
    [inst_2 : IsOpenImmersion f₁] [inst_3 : IsOpenImmersion f₂],
    (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f))
      (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
this✝¹ : IsAffine ↑↑U
this✝ : IsAffine ↑↑V
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
this : IsOpenImmersion g
e : ↑↑(pullback (↑U).ι (↑V).ι).toPresheafedSpace ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ IsCompact (↑↑U ∩ ↑↑V)

Proof state:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
    [inst_2 : IsOpenImmersion f₁] [inst_3 : IsOpenImmersion f₂],
    (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f))
      (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
this✝ : IsAffine ↑↑U
this : IsAffine ↑↑V
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
let g : pullback U.1.ι V.1.ι ⟶ X := pullback.fst _ _ ≫ U.1.ι

Result:
case mp
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂]
    [inst_2 : IsOpenImmersion f₁] [inst_3 : IsOpenImmersion f₂],
    (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f))
      (pullback.mapDesc f₁ f₂ f) ⋯
U V : ↑X.affineOpens
this✝ : IsAffine ↑↑U
this : IsAffine ↑↑V
g : pullback (↑U).ι (↑V).ι ⟶ X := pullback.fst (↑U).ι (↑V).ι ≫ (↑U).ι
⊢ IsCompact (↑↑U ∩ ↑↑V)