-- 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 mp
X : Scheme
⊢ (∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) →
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
intro H U V

Result:
case mp
X : Scheme
H : ∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
U V : ↑X.affineOpens
⊢ IsCompact (↑↑U ∩ ↑↑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), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
intro U V hU hU' hV hV'

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

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.carrier ∩ ↑↑V ∪ ↑↑W ∩ ↑↑V)

Tactic:
apply hW.union

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 (↑↑W ∩ ↑↑V)

Proof state:
case mpr.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
⊢ IsCompact (U ⊓ ⊥).carrier

Tactic:
simp

Result:
no goals

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.carrier ∪ ↑↑W) ∩ ↑↑V)

Tactic:
rw [Set.union_inter_distrib_right]

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 ∩ ↑↑V ∪ ↑↑W ∩ ↑↑V)

Proof state:
X : Scheme
⊢ (∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
constructor

Result:
case mp
X : Scheme
⊢ (∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) →
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

case mpr
X : Scheme
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ 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 ∩ (S.carrier ∪ ↑↑V))

Tactic:
rw [Set.inter_union_distrib_left]

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 ∪ U.carrier ∩ ↑↑V)

Proof state:
case mp
X : Scheme
H : ∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
U V : ↑X.affineOpens
⊢ IsCompact (↑↑U ∩ ↑↑V)

Tactic:
exact H U V U.1.2 U.2.isCompact V.1.2 V.2.isCompact

Result:
no goals

Proof state:
X : Scheme
⊢ QuasiSeparatedSpace ↑↑X.toPresheafedSpace ↔ ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
rw [quasiSeparatedSpace_iff]

Result:
X : Scheme
⊢ (∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Proof state:
case mpr
X : Scheme
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
intro H

Result:
case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
⊢ ∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Proof state:
case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
⊢ ∀ (U V : Set ↑↑X.toPresheafedSpace), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)

Tactic:
suffices
  ∀ (U : X.Opens) (_ : IsCompact U.1) (V : X.Opens) (_ : IsCompact V.1),
    IsCompact (U ⊓ V).1
  by intro U V hU hU' hV hV'; exact this ⟨U, hU⟩ hU' ⟨V, hV⟩ hV'

Result:
case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
⊢ ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier

Proof state:
case mpr
X : Scheme
H : ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
⊢ ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier

Tactic:
intro U hU V hV

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

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

Tactic:
refine compact_open_induction_on V hV ?_ ?_

Result:
case mpr.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
⊢ IsCompact (U ⊓ ⊥).carrier

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),
    IsCompact S.carrier → ∀ (U_1 : ↑X.affineOpens), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ ↑U_1)).carrier

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),
    IsCompact S.carrier → ∀ (U_1 : ↑X.affineOpens), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ ↑U_1)).carrier

Tactic:
intro S _ V 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
hV : IsCompact (U ⊓ S).carrier
⊢ IsCompact (U ⊓ (S ⊔ ↑V)).carrier

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 (↑↑W ∩ ↑↑V)

Tactic:
apply H

Result:
no goals