awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : ModuleCat (↑R : Type u)
⊢ Eq.{u + 1} (α := Submodule (↑R : Type u) (↑M : Type u)) (Submodule.span (↑R : Type u) Set.univ) ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
rw : (tilde.functor R).essImage M
⊢ IsIso M.fromTildeΓ

Tactic:
rw [isIso_fromTildeΓ_iff]

Premises used: AlgebraicGeometry.isIso_fromTildeΓ_iff
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
g : Quiver.Hom (V := ModuleCat (↑R : Type u)) (ModuleCat.of (↑R : Type u) (P.relations.I →₀ (↑R : Type u)))
  (ModuleCat.of (↑R : Type u) (P.generators.I →₀ (↑R : Type u))) :=
  (tilde.functor R).preimage
    (Iso.hom (tildeFinsupp P.relations.I) ≫
      P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I))
refine :
  (tilde.functor R).map g ≫ Iso.hom (tildeFinsupp P.generators.I) =
    Iso.hom (tildeFinsupp P.relations.I) ≫ P.relations.π ≫ kernel.ι P.generators.π
⊢ cokernel ((tilde.functor R).map g) ≅ cokernel (P.relations.π ≫ kernel.ι P.generators.π)

Tactic:
refine cokernel.mapIso _ _ (tildeFinsupp _) (tildeFinsupp _) ?_

Premises used: CategoryTheory.Limits.cokernel.mapIso, AlgebraicGeometry.tildeFinsupp
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
g : Quiver.Hom (V := ModuleCat (↑R : Type u)) (ModuleCat.of (↑R : Type u) (P.relations.I →₀ (↑R : Type u)))
  (ModuleCat.of (↑R : Type u) (P.generators.I →₀ (↑R : Type u))) :=
  (tilde.functor R).preimage
    (Iso.hom (tildeFinsupp P.relations.I) ≫
      P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I))
simp :
  (Iso.hom (tildeFinsupp P.relations.I) ≫
        P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I)) ≫
      Iso.hom (tildeFinsupp P.generators.I) =
    Iso.hom (tildeFinsupp P.relations.I) ≫ P.relations.π ≫ kernel.ι P.generators.π
⊢ (tilde.functor R).map g ≫ Iso.hom (tildeFinsupp P.generators.I) =
    Iso.hom (tildeFinsupp P.relations.I) ≫ P.relations.π ≫ kernel.ι P.generators.π

Tactic:
simp only [g, (tilde.functor R).map_preimage]

Premises used: AlgebraicGeometry.tilde.functor, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
g : Quiver.Hom (V := ModuleCat (↑R : Type u)) (ModuleCat.of (↑R : Type u) (P.relations.I →₀ (↑R : Type u)))
  (ModuleCat.of (↑R : Type u) (P.generators.I →₀ (↑R : Type u))) :=
  (tilde.functor R).preimage
    (Iso.hom (tildeFinsupp P.relations.I) ≫
      P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I))
⊢ (Iso.hom (tildeFinsupp P.relations.I) ≫
        P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I)) ≫
      Iso.hom (tildeFinsupp P.generators.I) =
    Iso.hom (tildeFinsupp P.relations.I) ≫ P.relations.π ≫ kernel.ι P.generators.π

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
g : Quiver.Hom (V := ModuleCat (↑R : Type u)) (ModuleCat.of (↑R : Type u) (P.relations.I →₀ (↑R : Type u)))
  (ModuleCat.of (↑R : Type u) (P.generators.I →₀ (↑R : Type u))) :=
  (tilde.functor R).preimage
    (Iso.hom (tildeFinsupp P.relations.I) ≫
      P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I))
iso : cokernel ((tilde.functor R).map g) ≅ cokernel (P.relations.π ≫ kernel.ι P.generators.π) :=
  cokernel.mapIso ((tilde.functor R).map g) (P.relations.π ≫ kernel.ι P.generators.π) (tildeFinsupp P.relations.I)
    (tildeFinsupp P.generators.I) ⋯
⊢ (tilde.functor R).essImage M

Tactic:
⟨cokernel g, ⟨PreservesCokernel.iso (tilde.functor R) g ≪≫ iso ≪≫
    IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) P.isColimit⟩⟩

Premises used: SheafOfModules.Presentation.isColimit, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.PreservesCokernel.iso, CategoryTheory.Limits.cokernel, CategoryTheory.Functor.essImage, Nonempty.intro, AlgebraicGeometry.tilde.functor, CategoryTheory.Iso.trans, Exists.intro, CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIso
-- Module: Mathlib.AlgebraicGeometry.Modules.Tilde
Goal:
R : CommRingCat
M : (Spec R).Modules
P : SheafOfModules.Presentation M
g : Quiver.Hom (V := ModuleCat (↑R : Type u)) (ModuleCat.of (↑R : Type u) (P.relations.I →₀ (↑R : Type u)))
  (ModuleCat.of (↑R : Type u) (P.generators.I →₀ (↑R : Type u))) :=
  (tilde.functor R).preimage
    (Iso.hom (tildeFinsupp P.relations.I) ≫
      P.relations.π ≫ kernel.ι P.generators.π ≫ Iso.inv (tildeFinsupp P.generators.I))
iso : cokernel ((tilde.functor R).map g) ≅ cokernel (P.relations.π ≫ kernel.ι P.generators.π) :=
  cokernel.mapIso ((tilde.functor R).map g) (P.relations.π ≫ kernel.ι P.generators.π) (tildeFinsupp P.relations.I)
    (tildeFinsupp P.generators.I) ⋯
⊢ (tilde.functor R).essImage M

Tactic:
exact ⟨cokernel g, ⟨PreservesCokernel.iso (tilde.functor R) g ≪≫ iso ≪≫
    IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) P.isColimit⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y : Scheme
U : Y.Opens
hU : IsAffineOpen U
f : X ⟶ Y
inst : IsAffineHom f
⊢ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
IsAffineHom.isAffine_preimage _ hU

Premises used: AlgebraicGeometry.IsAffineHom.isAffine_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
⊢ IsAffineHom f

Tactic:
⟨fun _ hU ↦ hU.preimage_of_isIso f⟩

Premises used: AlgebraicGeometry.IsAffineHom.mk, AlgebraicGeometry.IsAffineOpen.preimage_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
⊢ QuasiCompact f

Tactic:
quasiCompact_iff_forall_isAffineOpen.mpr fun _ hU ↦ (hU.preimage f).isCompact

Premises used: Iff.mpr, AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen, AlgebraicGeometry.IsAffineOpen.preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
isAffine_preimage : ∀ (U : Z.Opens), IsAffineOpen U → IsAffineOpen ((f ≫ g) ⁻¹ᵁ U)
⊢ IsAffineHom (f ≫ g)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
isAffine_preimage : IsAffineOpen ((Opens.map f.base).obj ((Opens.map g.base).obj U))
⊢ IsAffineOpen ((f ≫ g) ⁻¹ᵁ U)

Tactic:
rw [Scheme.Hom.comp_base, Opens.map_comp_obj]

Premises used: TopologicalSpace.Opens.map_comp_obj, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
isAffine_preimage : IsAffineOpen ((Opens.map g.base).obj U)
⊢ IsAffineOpen ((Opens.map f.base).obj ((Opens.map g.base).obj U))

Tactic:
apply IsAffineHom.isAffine_preimage

Premises used: AlgebraicGeometry.IsAffineHom.isAffine_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
U : Z.Opens
hU isAffine_preimage : IsAffineOpen U
⊢ IsAffineOpen ((Opens.map g.base).obj U)

Tactic:
apply IsAffineHom.isAffine_preimage

Premises used: AlgebraicGeometry.IsAffineHom.isAffine_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen U

Tactic:
hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsAffineHom f
inst_1 : IsAffineHom g
U : Z.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen U

Tactic:
exact hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
isAffine_preimage : ∀ (U : X.Opens), IsAffineOpen U → IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)
⊢ IsAffineHom (X.basicOpen r).ι

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
isAffine_preimage : IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)
⊢ IsAffineOpen ((X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
fapply (Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion (X.basicOpen r).ι).mp

Premises used: AlgebraicGeometry.Scheme.Hom.isAffineOpen_iff_of_isOpenImmersion, AlgebraicGeometry.Scheme.basicOpen, Iff.mp, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
⊢ IsAffineOpen
    (X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op ⊤)) (Y := X.presheaf.obj (op U))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u_1)) → (↑(X.presheaf.obj (op U)) : Type u_1))
        r))

Tactic:
hU.basicOpen (X.presheaf.map (homOfLE le_top).op r)

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
h :
  (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op ⊤)) (Y := X.presheaf.obj (op U))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u_1)) → (↑(X.presheaf.obj (op U)) : Type u_1))
        r)
⊢ IsAffineOpen ((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U)

Tactic:
convert! hU.basicOpen (X.presheaf.map (homOfLE le_top).op r)

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
h : (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U = U ⊓ X.basicOpen r
⊢ (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U =
    X.basicOpen (U := U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op ⊤)) (Y := X.presheaf.obj (op U))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑(X.presheaf.obj (op ⊤)) : Type u_1)) → (↑(X.presheaf.obj (op U)) : Type u_1))
        r)

Tactic:
rw [X.basicOpen_res]

Premises used: AlgebraicGeometry.Scheme.basicOpen_res
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
h : (↑((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U) : Set ↥X) = (↑(U ⊓ X.basicOpen r) : Set ↥X)
⊢ (X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U = U ⊓ X.basicOpen r

Tactic:
ext1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
⊢ (↑((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U) : Set ↥X) = (↑(U ⊓ X.basicOpen r) : Set ↥X)

Tactic:
Set.image_preimage_eq_inter_range.trans ?_

Premises used: Set.Mem, setOf, Set.image_preimage_eq_inter_range, Set.preimage, Set.image, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
h : U.1 ∩ Set.range (ι := ↥(↑(X.basicOpen r) : Scheme)) ⇑(X.basicOpen r).ι = (↑(U ⊓ X.basicOpen r) : Set ↥X)
⊢ (↑((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U) : Set ↥X) = (↑(U ⊓ X.basicOpen r) : Set ↥X)

Tactic:
refine Set.image_preimage_eq_inter_range.trans ?_

Premises used: Set.image_preimage_eq_inter_range, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
r : (↑Γ(X, ⊤) : Type u_1)
U : X.Opens
hU : IsAffineOpen U
⊢ U.1 ∩ Set.range (ι := ↥(↑(X.basicOpen r) : Scheme)) ⇑(X.basicOpen r).ι = (↑(U ⊓ X.basicOpen r) : Set ↥X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : (↑Γ(X, ⊤) : Type u)
⊢ IsRetrocompact (↑(X.basicOpen s) : Set ↥X)

Tactic:
IsRetrocompact_iff_isSpectralMap_subtypeVal.mpr (X.basicOpen s).ι.isSpectralMap

Premises used: Iff.mpr, IsRetrocompact_iff_isSpectralMap_subtypeVal, AlgebraicGeometry.Scheme.Hom.isSpectralMap, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
rw : ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
rw [quasiSeparatedSpace_iff_forall_affineOpens]

Premises used: AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
obtain :
  ∀ (s' : Finset (↑Γ(X, ⊤) : Type u)) (hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s)
    (e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤),
    IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
obtain ⟨s', hs', e⟩ := (Ideal.span_eq_top_iff_finite _).mp hs

Premises used: Ideal.span_eq_top_iff_finite, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
rw :
  IsCompact.{u} (X := ↥X)
    (⋃ (i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)),
      (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
rw [← Set.inter_univ (_ ∩ _), ← Opens.coe_top, ← iSup_basicOpen_of_span_eq_top _ _ e,
    ← iSup_subtype'', Opens.coe_iSup, Set.inter_iUnion]

Premises used: TopologicalSpace.Opens.coe_iSup, Set.inter_univ, iSup_subtype'', AlgebraicGeometry.iSup_basicOpen_of_span_eq_top, Inter.inter, Set.inter_iUnion, TopologicalSpace.Opens.coe_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
h :
  ∀ (i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)),
    IsCompact
      ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
⊢ IsCompact.{u} (X := ↥X)
    (⋃ (i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)),
      (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))

Tactic:
apply isCompact_iUnion

Premises used: isCompact_iUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
h :
  IsCompact
    ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X) ∩
      ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X)))
⊢ IsCompact
    ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))

Tactic:
rw [Set.inter_inter_distrib_right]

Premises used: Set.inter_inter_distrib_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact
    ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X) ∩
      ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X)))

Tactic:
(hs₂ i (hs' i.2)).isQuasiSeparated _ _ Set.inter_subset_right
    (U.1.2.inter (X.basicOpen _).2) ?_ Set.inter_subset_right (V.1.2.inter (X.basicOpen _).2) ?_

Premises used: AlgebraicGeometry.Scheme.basicOpen, IsOpen.inter, TopologicalSpace.Opens.is_open', AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, Subtype.val, Set.inter_subset_right, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
h : IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
h₁ : IsCompact ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))
⊢ IsCompact
    ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X) ∩
      ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X)))

Tactic:
refine (hs₂ i (hs' i.2)).isQuasiSeparated _ _ Set.inter_subset_right
    (U.1.2.inter (X.basicOpen _).2) ?_ Set.inter_subset_right (V.1.2.inter (X.basicOpen _).2) ?_

Premises used: AlgebraicGeometry.Scheme.basicOpen, IsOpen.inter, TopologicalSpace.Opens.is_open', AlgebraicGeometry.IsAffineOpen.isQuasiSeparated, Subtype.val, Set.inter_subset_right, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
h :
  IsCompact
    (↑(X.basicOpen (U := (↑U : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
            (↑i : (↑Γ(X, ⊤) : Type u)))) :
      Set ↥X)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))

Tactic:
rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]

Premises used: Quiver.Hom.op, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.basicOpen_res, TopologicalSpace.Opens.coe_inf
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact
    (↑(X.basicOpen (U := (↑U : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
            (↑i : (↑Γ(X, ⊤) : Type u)))) :
      Set ↥X)

Tactic:
(U.2.basicOpen _).isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.IsAffineOpen.basicOpen, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
⊢ IsCompact
    (↑(X.basicOpen (U := (↑U : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑U : X.Opens)))
                (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑U : X.Opens)) : Type u))
            (↑i : (↑Γ(X, ⊤) : Type u)))) :
      Set ↥X)

Tactic:
exact (U.2.basicOpen _).isCompact

Premises used: AlgebraicGeometry.IsAffineOpen.isCompact, AlgebraicGeometry.IsAffineOpen.basicOpen, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Affine
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
hs : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span s) ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
U V : (↑X.affineOpens : Type u)
s' : Finset (↑Γ(X, ⊤) : Type u)
hs' : (↑s' : Set (↑Γ(X, ⊤) : Type u)) ⊆ s
e : Eq (α := Ideal (↑Γ(X, ⊤) : Type u)) (Ideal.span (↑s' : Set (↑Γ(X, ⊤) : Type u))) ⊤
i : (↑(↑s' : Set (↑Γ(X, ⊤) : Type u)) : Type u)
h :
  IsCompact
    (↑(X.basicOpen (U := (↑V : X.Opens))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Γ(X, ⊤)) (Y := Γ(X, (↑V : X.Opens)))
                (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
              (a : (↑Γ(X, ⊤) : Type u)) → (↑Γ(X, (↑V : X.Opens)) : Type u))
            (↑i : (↑Γ(X, ⊤) : Type u)))) :
      Set ↥X)
⊢ IsCompact ((↑(↑V : X.Opens) : Set ↥X) ∩ (↑(X.basicOpen (↑i : (↑Γ(X, ⊤) : Type u))) : Set ↥X))

Tactic:
rw [← Opens.coe_inf, ← X.basicOpen_res _ (homOfLE le_top).op]

Premises used: Quiver.Hom.op, le_top, CategoryTheory.homOfLE, AlgebraicGeometry.Scheme.basicOpen_res, TopologicalSpace.Opens.coe_inf