awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h : IsOpen U
hU' : IsCompact U
⊢ Function.RightInverse (⇑f) (TopCat.Hom.hom (inv f.base)).toFun

Tactic:
IsIso.hom_inv_id_apply f.base

Premises used: Function.LeftInverse, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Function.RightInverse, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.IsIso.hom_inv_id_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIso f
U : Set ↥Y
h : IsOpen U
hU' : IsCompact U
⊢ Function.RightInverse (⇑f) (TopCat.Hom.hom (inv f.base)).toFun

Tactic:
exact IsIso.hom_inv_id_apply f.base

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.IsIso.hom_inv_id_apply
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
isCompact_preimage : ∀ (U : Set ↥Z), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑(f ≫ g) ⁻¹' U)
⊢ QuasiCompact (f ≫ g)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
isCompact_preimage : IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⇑g ⁻¹' U))
⊢ IsCompact (X := ↥X) (⇑(f ≫ g) ⁻¹' U)

Tactic:
rw [Scheme.Hom.comp_base, TopCat.coe_comp, Set.preimage_comp]

Premises used: Set.preimage_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
isCompact_preimage : IsOpen (X := ↥Y) (⇑g ⁻¹' U)
isCompact_preimage₁ : IsCompact (X := ↥Y) (⇑g ⁻¹' U)
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⇑g ⁻¹' U))

Tactic:
apply QuasiCompact.isCompact_preimage

Premises used: AlgebraicGeometry.QuasiCompact.isCompact_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
⊢ Continuous (X := ↥Y) (Y := ↥Z) ⇑g

Tactic:
fun_prop
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
⊢ IsOpen (X := ↥Y) (⇑g ⁻¹' U)

Tactic:
exact Continuous.isOpen_preimage (by fun_prop) _ hU

Premises used: Continuous.isOpen_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
isCompact_preimage : IsOpen U
isCompact_preimage₁ : IsCompact U
⊢ IsCompact (X := ↥Y) (⇑g ⁻¹' U)

Tactic:
apply QuasiCompact.isCompact_preimage

Premises used: AlgebraicGeometry.QuasiCompact.isCompact_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
⊢ IsOpen U

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : QuasiCompact g
U : Set ↥Z
hU : IsOpen U
hU' : IsCompact U
⊢ IsCompact U

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : Set ↥X
hb : Opens.IsBasis.{u} (α := ↥X) (Set.range fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens))
hb' : ∀ (i : (↑X.affineOpens : Type u)), IsCompact (↑(↑i : X.Opens) : Set ↥X)
⊢ IsCompact U ∧ IsOpen U ↔ ∃ (s : Set (↑X.affineOpens : Type u)), s.Finite ∧ U = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)

Tactic:
apply Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion
    (fun (U : X.affineOpens) => (U : X.Opens))

Premises used: TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : Set ↥X
hb : Opens.IsBasis X.affineOpens
⊢ Opens.IsBasis.{u} (α := ↥X) (Set.range fun (U : (↑X.affineOpens : Type u)) ↦ (↑U : X.Opens))

Tactic:
rw [Subtype.range_coe]

Premises used: Subtype.range_coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis X.affineOpens

Tactic:
X.isBasis_affineOpens

Premises used: AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : Set ↥X
⊢ Opens.IsBasis X.affineOpens

Tactic:
exact X.isBasis_affineOpens

Premises used: AlgebraicGeometry.Scheme.isBasis_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : Set ↥X
⊢ ∀ (i : (↑X.affineOpens : Type u)), IsCompact (↑(↑i : X.Opens) : Set ↥X)

Tactic:
fun i => i.2.isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : Set ↥X
⊢ ∀ (i : (↑X.affineOpens : Type u)), IsCompact (↑(↑i : X.Opens) : Set ↥X)

Tactic:
exact fun i => i.2.isCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
⊢ IsCompact U.carrier ∧ IsOpen U.carrier ↔
    ∃ (s : Set (↑X.affineOpens : Type u)), s.Finite ∧ U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)

Tactic:
isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens (U := U.1)

Premises used: AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
h : IsCompact (↑U : Set ↥X) ↔ IsCompact U.carrier ∧ IsOpen U.carrier
h₁ :
  ∀ (s : Set (↑X.affineOpens : Type u)), U = ⨆ i ∈ s, (↑i : X.Opens) ↔ U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)
⊢ IsCompact (↑U : Set ↥X) ↔ ∃ (s : Set (↑X.affineOpens : Type u)), s.Finite ∧ U = ⨆ i ∈ s, (↑i : X.Opens)

Tactic:
convert! isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens (U := U.1) using 4 with s

Premises used: AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
⊢ IsCompact (↑U : Set ↥X) ↔ IsCompact U.carrier ∧ IsOpen U.carrier

Tactic:
simp [U.isOpen]

Premises used: TopologicalSpace.Opens.isOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
s : Set (↑X.affineOpens : Type u)
⊢ U = ⨆ i ∈ s, (↑i : X.Opens) ↔ (↑U : Set ↥X) = (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)

Tactic:
SetLike.coe_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, SetLike.coe_injective, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
s : Set (↑X.affineOpens : Type u)
h : ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X) = (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)
⊢ U = ⨆ i ∈ s, (↑i : X.Opens) ↔ U.carrier = ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X)

Tactic:
convert! SetLike.coe_injective.eq_iff.symm

Premises used: Function.Injective.eq_iff, SetLike.coe_injective, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
s : Set (↑X.affineOpens : Type u)
⊢ ⋃ i ∈ s, (↑(↑i : X.Opens) : Set ↥X) = (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
inst : IsAffine X
U : Set ↥X
⊢ IsCompact U ∧ IsOpen U ↔ ∃ (s : Set (↑Γ(X, ⊤) : Type u)), s.Finite ∧ U = ⋃ i ∈ s, (↑(X.basicOpen i) : Set ↥X)

Tactic:
(isBasis_basicOpen X).isCompact_open_iff_eq_finite_iUnion _
    (fun _ => ((isAffineOpen_top _).basicOpen _).isCompact) _

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.isBasis_basicOpen, TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
rw :
  (∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
⊢ QuasiCompact f ↔ ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)

Tactic:
rw [quasiCompact_iff]

Premises used: AlgebraicGeometry.quasiCompact_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)

Tactic:
⟨fun H U hU => H U U.isOpen hU.isCompact, ?_⟩

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, SetLike.coe, TopologicalSpace.Opens.isOpen, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
refine :
  (∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)) →
    ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)
⊢ (∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (X := ↥X) (⇑f ⁻¹' U)) ↔
    ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)

Tactic:
refine ⟨fun H U hU => H U U.isOpen hU.isCompact, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
U : Set ↥Y
hU : IsOpen U
hU' : IsCompact U
obtain :
  ∀ (S : Set (↑Y.affineOpens : Type u)) (hS : S.Finite)
    (hU : IsOpen.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y)))
    (hU' : IsCompact.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))),
    IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y)))
⊢ IsCompact (X := ↥X) (⇑f ⁻¹' U)

Tactic:
obtain ⟨S, hS, rfl⟩ := isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp ⟨hU', hU⟩

Premises used: AlgebraicGeometry.isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens, And.intro, Iff.mp, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
S : Set (↑Y.affineOpens : Type u)
hS : S.Finite
hU : IsOpen.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))
hU' : IsCompact.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))
simp : IsCompact.{u} (X := ↥X) (⋃ i ∈ S, ⇑f ⁻¹' (↑(↑i : Y.Opens) : Set ↥Y))
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y)))

Tactic:
simp only [Set.preimage_iUnion]

Premises used: Set.preimage_iUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
S : Set (↑Y.affineOpens : Type u)
hS : S.Finite
hU : IsOpen.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))
hU' : IsCompact.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))
⊢ IsCompact.{u} (X := ↥X) (⋃ i ∈ S, ⇑f ⁻¹' (↑(↑i : Y.Opens) : Set ↥Y))

Tactic:
Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop)

Premises used: Set.Finite.isCompact_biUnion, Subtype.prop, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
H : ∀ (U : Y.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥X)
S : Set (↑Y.affineOpens : Type u)
hS : S.Finite
hU : IsOpen.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))
hU' : IsCompact.{u} (X := ↥Y) (⋃ i ∈ S, (↑(↑i : Y.Opens) : Set ↥Y))
⊢ IsCompact.{u} (X := ↥X) (⋃ i ∈ S, ⇑f ⁻¹' (↑(↑i : Y.Opens) : Set ↥Y))

Tactic:
exact Set.Finite.isCompact_biUnion hS (fun i _ => H i i.prop)

Premises used: Set.Finite.isCompact_biUnion, Subtype.prop, Subtype.val
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
⊢ IsCompact (↑(X.basicOpen f) : Set ↥X)

Tactic:
isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_

Premises used: Iff.mpr, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
refine : ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
⊢ IsCompact (↑(X.basicOpen f) : Set ↥X)

Tactic:
refine isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_

Premises used: Iff.mpr, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
obtain :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
⊢ ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)

Tactic:
obtain ⟨s, hs, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hU

Premises used: Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
V : (↑s : Type u_1)
rw :
  X.basicOpen (U := (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens)) : Type u_1))
        f) ∈
    X.affineOpens
⊢ (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f ∈ X.affineOpens

Tactic:
rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]

Premises used: LE.le.trans_eq, Quiver.Hom.op, le_iSup₂, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.basicOpen_res, Eq.symm, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
V : (↑s : Type u_1)
⊢ X.basicOpen (U := (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens)) : Type u_1))
        f) ∈
    X.affineOpens

Tactic:
V.1.2.basicOpen _

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, Set.Mem, setOf, AlgebraicGeometry.IsAffineOpen, AlgebraicGeometry.Scheme.affineOpens, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
V : (↑s : Type u_1)
⊢ X.basicOpen (U := (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, (↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens)) : Type u_1))
        f) ∈
    X.affineOpens

Tactic:
exact V.1.2.basicOpen _

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
⊢ Finite.{u_1 + 1} (↑s : Type u_1)

Tactic:
haveI : Finite s := hs.to_subtype
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
⊢ ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)

Tactic:
⟨Set.range g, Set.finite_range g, ?_⟩

Premises used: Set.finite_range, And.intro, Exists.intro, Set.range
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
refine : X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
⊢ ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)

Tactic:
refine ⟨Set.range g, Set.finite_range g, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
s : Set (↑X.affineOpens : Type u_1)
hs : s.Finite
e : U = ⨆ i ∈ s, (↑i : X.Opens)
g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) :=
  fun (V : (↑s : Type u_1)) ↦
    Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
      ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯
this : Finite.{u_1 + 1} (↑s : Type u_1)
rw : X.basicOpen f = ⨆ (i : (↑s : Type u_1)), (↑(g i) : X.Opens)
rw₁ : X.basicOpen f = (⨆ (i : (↑s : Type u_1)), (↑(↑i : (↑X.affineOpens : Type u_1)) : X.Opens)) ⊓ X.basicOpen f
rw₂ :
  X.basicOpen f =
    (⨆ (i : (↑X.affineOpens : Type u_1)),
        ⨆ (h : i ∈ s),
          (↑(↑(Subtype.mk (p := fun (x : (↑X.affineOpens : Type u_1)) ↦ x ∈ s) i h) : (↑X.affineOpens : Type u_1)) :
            X.Opens)) ⊓
      X.basicOpen f
rw₃ : X.basicOpen f = U ⊓ X.basicOpen f
rw₄ rw₅ : X.basicOpen f = X.basicOpen f
⊢ X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)

Tactic:
rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]

Premises used: Iff.mpr, iSup_subtype, iSup_range, AlgebraicGeometry.Scheme.basicOpen_le, iSup_inf_eq, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsCompact (↑U : Set ↥X)
f : (↑Γ(X, U) : Type u_1)
refine : ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₁ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₂ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₃ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens))
    (this : Finite.{u_1 + 1} (↑s : Type u_1)),
    ∃ (s : Set (↑X.affineOpens : Type u_1)), s.Finite ∧ X.basicOpen f = ⨆ i ∈ s, (↑i : X.Opens)
refine₄ :
  ∀ (s : Set (↑X.affineOpens : Type u_1)) (hs : s.Finite) (e : U = ⨆ i ∈ s, (↑i : X.Opens)),
    let g : (↑s : Type u_1) → (↑X.affineOpens : Type u_1) := fun (V : (↑s : Type u_1)) ↦
      Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens)
        ((↑(↑V : (↑X.affineOpens : Type u_1)) : X.Opens) ⊓ X.basicOpen f) ⋯;
    ∀ (this : Finite.{u_1 + 1} (↑s : Type u_1)), X.basicOpen f = ⨆ i ∈ Set.range g, (↑i : X.Opens)
⊢ IsCompact (↑(X.basicOpen f) : Set ↥X)

Tactic:
classical
  refine isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ?_
  obtain ⟨s, hs, e⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hU
  let g : s → X.affineOpens := fun V ↦ ⟨V.1 ⊓ X.basicOpen f, by
    rw [← X.basicOpen_res _ (homOfLE ((le_iSup₂ V.1 V.2).trans_eq e.symm)).op]
    exact V.1.2.basicOpen _⟩
  haveI : Finite s := hs.to_subtype
  refine ⟨Set.range g, Set.finite_range g, ?_⟩
  rw [iSup_range, ← iSup_inf_eq, iSup_subtype, ← e, inf_eq_right.mpr (X.basicOpen_le f)]

Premises used: Iff.mpr, iSup_subtype, iSup_range, AlgebraicGeometry.Scheme.basicOpen_le, iSup_inf_eq, Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, inf_eq_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
respectsIso :
  (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      CompactSpace.{u_1} ↥X).RespectsIso
to_basicOpen :
  ∀ {X Y : Scheme.{u_1}} [IsAffine Y] (f : X ⟶ Y) (r : (↑Γ(Y, ⊤) : Type u_1)),
    CompactSpace.{u_1} ↥X → CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
of_basicOpenCover :
  ∀ {X Y : Scheme.{u_1}} [IsAffine Y] (f : X ⟶ Y) (s : Finset (↑Γ(Y, ⊤) : Type u_1)),
    Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑s : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤ →
      (∀ (r : ↥s), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)) →
        CompactSpace.{u_1} ↥X
⊢ AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    CompactSpace.{u_1} ↥X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
respectsIso :
  ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥X
respectsIso₁ :
  ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], CompactSpace.{u_1} ↥X → CompactSpace.{u_1} ↥X
⊢ (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      CompactSpace.{u_1} ↥X).RespectsIso

Tactic:
apply AffineTargetMorphismProperty.respectsIso_mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.respectsIso_mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
X Y Z : Scheme
e : Y ≅ Z
f_1 : X ⟶ Y
inst : IsAffine Y
H : CompactSpace.{u_1} ↥X
⊢ CompactSpace.{u_1} ↥X

Tactic:
H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
X Y Z : Scheme
e : X ≅ Y
f_1 : Y ⟶ Z
inst : IsAffine Z
H : CompactSpace.{u_1} ↥Y
⊢ CompactSpace.{u_1} ↥X

Tactic:
exacts [@Homeomorph.compactSpace _ _ _ _ H (TopCat.homeoOfIso (asIso e.inv.base)), H]

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', TopCat.homeoOfIso, Homeomorph.compactSpace, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.inv, CategoryTheory.asIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u_1)
H : CompactSpace.{u_1} ↥X
to_basicOpen :
  CompactSpace.{u_1}
    ↥(↑(X.basicOpen (U := f ⁻¹ᵁ ⊤)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
                (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u_1))
              r)) :
        Scheme)
⊢ CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)

Tactic:
rw [Scheme.preimage_basicOpen f r]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen