-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem quasiSeparatedSpace_iff_affine (X : Scheme) :
    QuasiSeparatedSpace X ↔ ∀ U V : X.affineOpens, IsCompact (U ∩ V : Set X)

Proof state:
case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S✝ : X.Opens
x✝¹ : IsCompact S✝.carrier
V : ↑X.affineOpens
S : X.Opens
x✝ : IsCompact S.carrier
W : ↑X.affineOpens
hW : IsCompact (S.carrier ∩ ↑↑V)
⊢ IsCompact ((S ⊔ ↑W).carrier ∩ ↑↑V)

Tactic:
change IsCompact ((S.1 ∪ W.1) ∩ V.1)

Result:
case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S✝ : X.Opens
x✝¹ : IsCompact S✝.carrier
V : ↑X.affineOpens
S : X.Opens
x✝ : IsCompact S.carrier
W : ↑X.affineOpens
hW : IsCompact (S.carrier ∩ ↑↑V)
⊢ IsCompact ((S.carrier ∪ ↑↑W) ∩ ↑↑V)

Proof state:
case mpr.refine_2.refine_1
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ IsCompact (⊥.carrier ∩ ↑↑V)

Tactic:
simp

Result:
no goals

Proof state:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U ⊓ (S ⊔ ↑V)).carrier

Tactic:
change IsCompact (U.1 ∩ (S.1 ∪ V.1))

Result:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U.carrier ∩ (S.carrier ∪ ↑↑V))

Proof state:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ IsCompact (U.carrier ∩ ↑↑V)

Tactic:
refine compact_open_induction_on U hU ?_ ?_

Result:
case mpr.refine_2.refine_1
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ IsCompact (⊥.carrier ∩ ↑↑V)

case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier → ∀ (U : ↑X.affineOpens), IsCompact (S.carrier ∩ ↑↑V) → IsCompact ((S ⊔ ↑U).carrier ∩ ↑↑V)

Proof state:
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
this : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
U V : Set ↑↑X.toPresheafedSpace
hU : IsOpen U
hU' : IsCompact U
hV : IsOpen V
hV' : IsCompact V
⊢ IsCompact (U ∩ V)

Tactic:
exact this ⟨U, hU⟩ hU' ⟨V, hV⟩ hV'

Result:
no goals

Proof state:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U.carrier ∩ S.carrier ∪ U.carrier ∩ ↑↑V)

Tactic:
apply hV.union

Result:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U.carrier ∩ ↑↑V)

Proof state:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV✝ : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U.carrier ∩ ↑↑V)

Tactic:
clear hV

Result:
case mpr.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ IsCompact (U.carrier ∩ ↑↑V)

Proof state:
case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S : X.Opens
x✝ : IsCompact S.carrier
V : ↑X.affineOpens
⊢ ∀ (S : X.Opens),
    IsCompact S.carrier → ∀ (U : ↑X.affineOpens), IsCompact (S.carrier ∩ ↑↑V) → IsCompact ((S ⊔ ↑U).carrier ∩ ↑↑V)

Tactic:
intro S _ W hW

Result:
case mpr.refine_2.refine_2
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
U : X.Opens
hU : IsCompact U.carrier
V✝ : X.Opens
hV : IsCompact V✝.carrier
S✝ : X.Opens
x✝¹ : IsCompact S✝.carrier
V : ↑X.affineOpens
S : X.Opens
x✝ : IsCompact S.carrier
W : ↑X.affineOpens
hW : IsCompact (S.carrier ∩ ↑↑V)
⊢ IsCompact ((S ⊔ ↑W).carrier ∩ ↑↑V)