-- 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 mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
this : IsOpenImmersion g
⊢ CompactSpace ↑↑(pullback f₁ f₂).toPresheafedSpace

Tactic:
have e := Homeomorph.ofIsEmbedding _ this.base_open.isEmbedding

Result:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
this : IsOpenImmersion g
e : ↑↑(pullback f₁ f₂).toPresheafedSpace ≃ₜ ↑(Set.range ⇑(ConcreteCategory.hom (Scheme.Hom.toLRSHom g).base))
⊢ CompactSpace ↑↑(pullback f₁ f₂).toPresheafedSpace

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).ι
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
have : IsOpenImmersion g := inferInstance

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
⊢ 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 ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ CompactSpace ↑(↑↑U ∩ ↑↑V)

Tactic:
exact @Homeomorph.compactSpace _ _ _ _ (H _ _) e

Result:
no goals

Proof state:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x => CompactSpace ↑↑X.toPresheafedSpace) f ↔
    QuasiSeparatedSpace ↑↑X.toPresheafedSpace

Tactic:
delta AffineTargetMorphismProperty.diagonal

Result:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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) ⋯) ↔
    QuasiSeparatedSpace ↑↑X.toPresheafedSpace

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 ≃ₜ ↑(↑↑U ∩ ↑↑V)
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
rw [isCompact_iff_compactSpace]

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)
⊢ CompactSpace ↑(↑↑U ∩ ↑↑V)

Proof state:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
⊢ CompactSpace ↑↑(pullback f₁ f₂).toPresheafedSpace

Tactic:
let g : pullback f₁ f₂ ⟶ X := pullback.fst _ _ ≫ f₁

Result:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
⊢ CompactSpace ↑↑(pullback f₁ f₂).toPresheafedSpace

Proof state:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
this : IsOpenImmersion g
e :
  ↑↑(pullback f₁ f₂).toPresheafedSpace ≃ₜ
    ↑(Set.range ⇑(ConcreteCategory.hom f₁.base) ∩ Set.range ⇑(ConcreteCategory.hom f₂.base))
⊢ CompactSpace ↑↑(pullback f₁ f₂).toPresheafedSpace

Tactic:
simp_rw [isCompact_iff_compactSpace] at H

Result:
case mpr
X Y : Scheme
inst✝² : IsAffine Y
f : X ⟶ Y
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst✝¹ : IsAffine U₁
inst✝ : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
this : IsOpenImmersion g
e :
  ↑↑(pullback f₁ f₂).toPresheafedSpace ≃ₜ
    ↑(Set.range ⇑(ConcreteCategory.hom f₁.base) ∩ Set.range ⇑(ConcreteCategory.hom f₂.base))
H : ∀ (U V : ↑X.affineOpens), CompactSpace ↑(↑↑U ∩ ↑↑V)
⊢ CompactSpace ↑↑(pullback f₁ f₂).toPresheafedSpace

Proof state:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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) ⋯) ↔
    QuasiSeparatedSpace ↑↑X.toPresheafedSpace

Tactic:
rw [quasiSeparatedSpace_iff_affine]

Result:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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)