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

Tactic:
constructor

Result:
case mp
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)

case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ ⦃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) ⋯

Proof state:
case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ ⦃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) ⋯

Tactic:
introv H h₁ h₂

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₂
⊢ 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).ι
this : IsOpenImmersion g
⊢ IsCompact (↑↑U ∩ ↑↑V)

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

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 (Scheme.Hom.toLRSHom g).base))
⊢ IsCompact (↑↑U ∩ ↑↑V)

Proof state:
case mp
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)

Tactic:
intro H U V

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

Proof state:
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

Tactic:
exact
  @Homeomorph.compactSpace _ _ _ _
    (H ⟨⟨_, h₁.base_open.isOpen_range⟩, isAffineOpen_opensRange _⟩
      ⟨⟨_, h₂.base_open.isOpen_range⟩, isAffineOpen_opensRange _⟩)
    e.symm

Result:
no goals

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₁
⊢ CompactSpace ↑↑(pullback f₁ f₂).toPresheafedSpace

Tactic:
have : IsOpenImmersion g := inferInstance

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
⊢ 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 (Scheme.Hom.toLRSHom g).base))
⊢ CompactSpace ↑↑(pullback f₁ f₂).toPresheafedSpace

Tactic:
rw [IsOpenImmersion.range_pullback_to_base_of_left] at e

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 f₁.base) ∩ Set.range ⇑(ConcreteCategory.hom f₂.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
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
haveI : IsAffine _ := V.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
this : IsAffine ↑↑V
⊢ IsCompact (↑↑U ∩ ↑↑V)