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
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u_1)
H : CompactSpace.{u_1} ↥X
⊢ 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)

Tactic:
(isCompact_iff_compactSpace.mp (isCompact_basicOpen _ isCompact_univ _))

Premises used: isCompact_iff_compactSpace, Iff.mp, AlgebraicGeometry.isCompact_basicOpen
-- 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
⊢ 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)

Tactic:
exact (isCompact_iff_compactSpace.mp (isCompact_basicOpen _ isCompact_univ _))

Premises used: isCompact_iff_compactSpace, Iff.mp, AlgebraicGeometry.isCompact_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑S : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hS' : ∀ (r : ↥S), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
⊢ Eq.{u_1 + 1} (α := Y.Opens)
    (⨆ (f : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)), Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⊤

Tactic:
rw [← (isAffineOpen_top _).iSup_basicOpen_eq_self_iff] at hS

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑S : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hS' : ∀ (r : ↥S), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
hS₁ :
  Eq.{u_1 + 1} (α := Y.Opens)
    (⨆ (f : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)), Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⊤
⊢ ∀ (r : ↥S), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)

Tactic:
rw [← (isAffineOpen_top _).iSup_basicOpen_eq_self_iff] at hS

Premises used: AlgebraicGeometry.isAffineOpen_top, AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS :
  Eq.{u_1 + 1} (α := Y.Opens)
    (⨆ (f : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)), Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⊤
hS' : ∀ (r : ↥S), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
of_basicOpenCover :
  IsCompact.{u_1} (X := ↥X)
    (⋃ (i : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)),
      Opens.carrier ((Opens.map f.base).1 (Y.basicOpen (↑i : (↑Γ(Y, ⊤) : Type u_1)))))
⊢ CompactSpace.{u_1} ↥X

Tactic:
rw [← isCompact_univ_iff, ← Opens.coe_top, ← f.preimage_top, ← hS, Scheme.Hom.preimage_iSup,
        Opens.iSup_mk, Opens.coe_mk]

Premises used: TopologicalSpace.Opens.iSup_mk, AlgebraicGeometry.Scheme.Hom.preimage_top, AlgebraicGeometry.Scheme.Hom.preimage_iSup, TopologicalSpace.Opens.coe_mk, isCompact_univ_iff, TopologicalSpace.Opens.coe_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS :
  Eq.{u_1 + 1} (α := Y.Opens)
    (⨆ (f : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)), Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⊤
hS' : ∀ (r : ↥S), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
⊢ IsCompact.{u_1} (X := ↥X)
    (⋃ (i : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)),
      Opens.carrier ((Opens.map f.base).1 (Y.basicOpen (↑i : (↑Γ(Y, ⊤) : Type u_1)))))

Tactic:
isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i)

Premises used: Iff.mpr, isCompact_iff_compactSpace, isCompact_iUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS :
  Eq.{u_1 + 1} (α := Y.Opens)
    (⨆ (f : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)), Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⊤
hS' : ∀ (r : ↥S), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
⊢ IsCompact.{u_1} (X := ↥X)
    (⋃ (i : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)),
      Opens.carrier ((Opens.map f.base).1 (Y.basicOpen (↑i : (↑Γ(Y, ⊤) : Type u_1)))))

Tactic:
exact isCompact_iUnion fun i => isCompact_iff_compactSpace.mpr (hS' i)

Premises used: Iff.mpr, isCompact_iff_compactSpace, isCompact_iUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    QuasiCompact f ↔
      targetAffineLocally (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X) f
⊢ @QuasiCompact = targetAffineLocally fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ (U : Y.Opens), IsAffineOpen U → CompactSpace.{u_1} (↑(↑(f ⁻¹ᵁ U) : Set ↥X) : Type u_1)) ↔
    ∀ (a : Y.Opens) (b : a ∈ Y.affineOpens), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ a) : Scheme)
⊢ QuasiCompact f ↔
    targetAffineLocally (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X) f

Tactic:
simp only [quasiCompact_iff_forall_isAffineOpen, isCompact_iff_compactSpace,
      targetAffineLocally, Subtype.forall]

Premises used: isCompact_iff_compactSpace, Subtype.forall, AlgebraicGeometry.targetAffineLocally, AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → CompactSpace.{u_1} (↑(↑(f ⁻¹ᵁ U) : Set ↥X) : Type u_1)) ↔
    ∀ (a : Y.Opens) (b : a ∈ Y.affineOpens), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ a) : Scheme)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
rw rw₁ : CompactSpace.{u_1} ↥X ↔ CompactSpace.{u_1} ↥X
⊢ CompactSpace.{u_1} ↥X ↔ QuasiCompact (Y := ⊤_ Scheme) (terminal.from X)

Tactic:
rw [HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)]

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : CompactSpace.{u_1} ↥X
⊢ QuasiCompact X.toSpecΓ

Tactic:
HasAffineProperty.iff_of_isAffine.mpr ‹_›

Premises used: Iff.mpr, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : CompactSpace.{u} ↥Y
isCompact_univ : IsCompact.{u} (X := ↥X) Set.univ
⊢ CompactSpace.{u} ↥X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : CompactSpace.{u} ↥Y
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) Set.univ)

Tactic:
QuasiCompact.isCompact_preimage _ isOpen_univ CompactSpace.isCompact_univ

Premises used: AlgebraicGeometry.QuasiCompact.isCompact_preimage, CompactSpace.isCompact_univ, isOpen_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : CompactSpace.{u} ↥Y
⊢ IsCompact (X := ↥X) (Set.preimage (β := ↥Y) (⇑f) Set.univ)

Tactic:
exact QuasiCompact.isCompact_preimage _ isOpen_univ CompactSpace.isCompact_univ

Premises used: AlgebraicGeometry.QuasiCompact.isCompact_preimage, CompactSpace.isCompact_univ, isOpen_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
hP' :
  AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    CompactSpace.{u_1} ↥X
⊢ MorphismProperty.IsStableUnderBaseChange @QuasiCompact

Tactic:
apply HasAffineProperty.isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasAffineProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
hP' :
  ∀ ⦃X Y S : Scheme.{u_1}⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
    CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥(pullback f g)
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    CompactSpace.{u_1} ↥X

Tactic:
apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk

Premises used: AlgebraicGeometry.AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
hP' : ∀ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥(pullback f g)
⊢ ∀ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥(pullback f g)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f : X_1 ⟶ Y_1
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
hP' : ∀ [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥(pullback f g)
⊢ ∀ [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S), CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥(pullback f g)

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
dsimp : Finite.{u_1 + 1} Y.affineCover.finiteSubcover.I₀
⊢ Finite.{u_1 + 1} 𝒰.I₀

Tactic:
dsimp [𝒰]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ Finite.{u_1 + 1} Y.affineCover.finiteSubcover.I₀

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ Finite.{u_1 + 1} 𝒰.I₀

Tactic:
have : Finite 𝒰.I₀ := by dsimp [𝒰]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this_1 : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite.{u_1 + 1} 𝒰.I₀
i : 𝒰.I₀
dsimp :
  CompactSpace.{u_1}
    ↥(pullback (Y := Y.affineCover.X (Scheme.Cover.idx Y.affineCover (↑i : ↥Y))) f
        (Y.affineCover.f (Scheme.Cover.idx Y.affineCover (↑i : ↥Y)) ≫ g))
⊢ CompactSpace.{u_1} ↥(𝒰.X i)

Tactic:
dsimp [𝒰]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this_1 : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite.{u_1 + 1} 𝒰.I₀
i : 𝒰.I₀
⊢ CompactSpace.{u_1}
    ↥(pullback (Y := Y.affineCover.X (Scheme.Cover.idx Y.affineCover (↑i : ↥Y))) f
        (Y.affineCover.f (Scheme.Cover.idx Y.affineCover (↑i : ↥Y)) ≫ g))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this_1 : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite.{u_1 + 1} 𝒰.I₀
⊢ ∀ (i : 𝒰.I₀), CompactSpace.{u_1} ↥(𝒰.X i)

Tactic:
have : ∀ i, CompactSpace (𝒰.X i) := by intro i; dsimp [𝒰]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this_1 : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this_2 : Finite.{u_1 + 1} 𝒰.I₀
this : ∀ (i : 𝒰.I₀), CompactSpace.{u_1} ↥(𝒰.X i)
⊢ CompactSpace.{u_1} ↥(pullback f g)

Tactic:
𝒰.compactSpace

Premises used: AlgebraicGeometry.Scheme.OpenCover.compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this_1 : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this_2 : Finite.{u_1 + 1} 𝒰.I₀
this : ∀ (i : 𝒰.I₀), CompactSpace.{u_1} ↥(𝒰.X i)
⊢ CompactSpace.{u_1} ↥(pullback f g)

Tactic:
exact 𝒰.compactSpace

Premises used: AlgebraicGeometry.Scheme.OpenCover.compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f_1 : X ⟶ Y
Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : QuasiCompact g
⊢ QuasiCompact (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f_1 : X ⟶ Y
Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : QuasiCompact f
⊢ QuasiCompact (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f_1 : X ⟶ Y
Z : Scheme
f : X ⟶ Y
V : Y.Opens
inst : QuasiCompact f
⊢ QuasiCompact (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f_1 : X ⟶ Y
Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : QuasiCompact f
inst_1 : CompactSpace.{u} ↥Y
⊢ CompactSpace.{u} ↥(pullback f g)

Tactic:
QuasiCompact.compactSpace_of_compactSpace (pullback.snd _ _)

Premises used: CategoryTheory.Limits.pullback.snd, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f_1 : X ⟶ Y
Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
inst : QuasiCompact g
inst_1 : CompactSpace.{u} ↥X
⊢ CompactSpace.{u} ↥(pullback f g)

Tactic:
QuasiCompact.compactSpace_of_compactSpace (pullback.fst _ _)

Premises used: AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
⊢ IsCompact (↑U : Set ↥X) ↔ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)

Tactic:
isCompact_iff_compactSpace.trans ((compactSpace_iff_exists (X := U)).trans ?_)

Premises used: isCompact_iff_compactSpace, AlgebraicGeometry.compactSpace_iff_exists, Iff.trans
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
refine :
  (∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)),
      Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f) ↔
    ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
⊢ IsCompact (↑U : Set ↥X) ↔ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)

Tactic:
refine isCompact_iff_compactSpace.trans ((compactSpace_iff_exists (X := U)).trans ?_)

Premises used: isCompact_iff_compactSpace, AlgebraicGeometry.compactSpace_iff_exists, Iff.trans
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)), Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f
R : CommRingCat
f : Spec R ⟶ (↑U : Scheme)
hf : Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f
⊢ Set.range (ι := ↥(Spec R)) ⇑(f ≫ U.ι) = (↑U : Set ↥X)

Tactic:
simp [hf.range_comp]

Premises used: Function.Surjective.range_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
refine :
  (∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)) →
    ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ X) (hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)),
      ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)),
        Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f
⊢ (∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)),
      Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f) ↔
    ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)

Tactic:
refine ⟨fun ⟨R, f, hf⟩ ↦ ⟨R, f ≫ U.ι, by simp [hf.range_comp]⟩, fun ⟨R, f, hf⟩ ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
⊢ Subset (α := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑f) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
simp [hf]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
refine : Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑(IsOpenImmersion.lift U.ι f ⋯)
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)), Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f

Tactic:
refine ⟨R, IsOpenImmersion.lift U.ι f (by simp [hf]), ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
rw : Eq (α := Set ↥(↑U : Scheme)) (Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯)) Set.univ
⊢ Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑(IsOpenImmersion.lift U.ι f ⋯)

Tactic:
rw [← Set.range_eq_univ]

Premises used: Set.range_eq_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
a :
  Eq.{u + 1} (α := Set ↥X)
    ((fun (x : Set ↥(↑U : Scheme)) ↦ (⇑U.ι '' x : Set ↥X)) (Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯)))
    ((fun (x : Set ↥(↑U : Scheme)) ↦ (⇑U.ι '' x : Set ↥X)) Set.univ)
⊢ Eq (α := Set ↥(↑U : Scheme)) (Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯)) Set.univ

Tactic:
apply show Function.Injective (U.ι '' ·) from Set.image_val_injective

Premises used: Set.image_val_injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
a : (fun (a : ↥(↑U : Scheme)) ↦ U.ι a) '' Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯) = (↑U : Set ↥X)
⊢ Eq.{u + 1} (α := Set ↥X)
    ((fun (x : Set ↥(↑U : Scheme)) ↦ (⇑U.ι '' x : Set ↥X)) (Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯)))
    ((fun (x : Set ↥(↑U : Scheme)) ↦ (⇑U.ι '' x : Set ↥X)) Set.univ)

Tactic:
simp only [Set.image_univ, Scheme.Opens.range_ι]

Premises used: Set.image_univ, AlgebraicGeometry.Scheme.Opens.range_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
a : Set.range (ι := ↥(Spec R)) ((fun (a : ↥(↑U : Scheme)) ↦ U.ι a) ∘ ⇑(IsOpenImmersion.lift U.ι f ⋯)) = (↑U : Set ↥X)
a₁ :
  Set.range (ι := ↥(Spec R))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((IsOpenImmersion.lift U.ι f ⋯).base ≫ U.ι.base)) :
        (a : ↥(Spec R)) → ↥X) =
    (↑U : Set ↥X)
a₂ : Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι) = (↑U : Set ↥X)
a₃ a₄ a₅ a₆ : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
⊢ (fun (a : ↥(↑U : Scheme)) ↦ U.ι a) '' Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯) = (↑U : Set ↥X)

Tactic:
rwa [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsOpenImmersion.lift_fac]

Premises used: Set.range_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f ↔ SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
⟨fun h ↦ h.specializingMap, fun H ↦ ?_⟩

Premises used: Iff.intro, IsClosedMap.specializingMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
refine : ∀ (H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f ↔ SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
refine ⟨fun h ↦ h.specializingMap, fun H ↦ ?_⟩