awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw : QuasiSeparatedSpace.{u} (↑(↑U : Set ↥X) : Type u)
hs : IsOpen (↑U : Set ↥X)
⊢ IsQuasiSeparated (↑U : Set ↥X)

Tactic:
rw [isQuasiSeparated_iff_quasiSeparatedSpace]

Premises used: isQuasiSeparated_iff_quasiSeparatedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ QuasiSeparatedSpace.{u} (↑(↑U : Set ↥X) : Type u)

Tactic:
@AlgebraicGeometry.quasiSeparatedSpace_of_isAffine _ hU

Premises used: Set.Mem, AlgebraicGeometry.quasiSeparatedSpace_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsOpen (↑U : Set ↥X)

Tactic:
U.isOpen

Premises used: TopologicalSpace.Opens.isOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ QuasiSeparatedSpace.{u} (↑(↑U : Set ↥X) : Type u)

Tactic:
exacts [@AlgebraicGeometry.quasiSeparatedSpace_of_isAffine _ hU, U.isOpen]

Premises used: AlgebraicGeometry.quasiSeparatedSpace_of_isAffine, TopologicalSpace.Opens.isOpen
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst : QuasiSeparatedSpace.{u} ↥X
⊢ QuasiSeparated X.toSpecΓ

Tactic:
HasAffineProperty.iff_of_isAffine.mpr ‹_›

Premises used: Iff.mpr, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact ((↑(U i) : Set ↥X) ∩ (↑(U j) : Set ↥X))
this : AffineTargetMorphismProperty.IsLocal.{u} fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u} ↥X :=
  ⋯
rw :
  AffineTargetMorphismProperty.diagonal (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X)
    X.toSpecΓ
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
rw [← quasiCompact_affineProperty_iff_quasiSeparatedSpace X.toSpecΓ]

Premises used: AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace, AlgebraicGeometry.Scheme.toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact ((↑(U i) : Set ↥X) ∩ (↑(U j) : Set ↥X))
this : AffineTargetMorphismProperty.IsLocal.{u} fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u} ↥X :=
  ⋯
⊢ ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine.{u} ((X.openCoverOfIsOpenCover U hU).X i)

Tactic:
have : ∀ i, IsAffine ((X.openCoverOfIsOpenCover U hU).X i) := hU₁
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact ((↑(U i) : Set ↥X) ∩ (↑(U j) : Set ↥X))
this_1 : AffineTargetMorphismProperty.IsLocal.{u} fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u} ↥X :=
  ⋯
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine.{u} ((X.openCoverOfIsOpenCover U hU).X i)
⊢ AffineTargetMorphismProperty.diagonal (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X)
    X.toSpecΓ

Tactic:
AffineTargetMorphismProperty.diagonal_of_openCover_source _
    (Scheme.openCoverOfIsOpenCover _ _ hU) fun i j ↦ ?_

Premises used: AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_openCover_source
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact ((↑(U i) : Set ↥X) ∩ (↑(U j) : Set ↥X))
this_1 : AffineTargetMorphismProperty.IsLocal.{u} fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u} ↥X :=
  ⋯
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine.{u} ((X.openCoverOfIsOpenCover U hU).X i)
refine :
  ∀ (i j : (X.openCoverOfIsOpenCover U hU).I₀),
    CompactSpace.{u} ↥(pullback ((X.openCoverOfIsOpenCover U hU).f i) ((X.openCoverOfIsOpenCover U hU).f j))
⊢ AffineTargetMorphismProperty.diagonal (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X)
    X.toSpecΓ

Tactic:
refine AffineTargetMorphismProperty.diagonal_of_openCover_source _
    (Scheme.openCoverOfIsOpenCover _ _ hU) fun i j ↦ ?_

Premises used: AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, AlgebraicGeometry.AffineTargetMorphismProperty.diagonal_of_openCover_source
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact ((↑(U i) : Set ↥X) ∩ (↑(U j) : Set ↥X))
this_1 : AffineTargetMorphismProperty.IsLocal.{u} fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u} ↥X :=
  ⋯
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine.{u} ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
rw :
  IsCompact (X := ↥X)
    (Set.range (ι := ↥((X.openCoverOfIsOpenCover U hU).X i)) ⇑((X.openCoverOfIsOpenCover U hU).f i) ∩
      Set.range (ι := ↥((X.openCoverOfIsOpenCover U hU).X j)) ⇑((X.openCoverOfIsOpenCover U hU).f j))
⊢ CompactSpace.{u} ↥(pullback ((X.openCoverOfIsOpenCover U hU).f i) ((X.openCoverOfIsOpenCover U hU).f j))

Tactic:
rw [← isCompact_univ_iff, (pullback.fst ((X.openCoverOfIsOpenCover U hU).f i)
    ((X.openCoverOfIsOpenCover U hU).f j) ≫
    (X.openCoverOfIsOpenCover U hU).f i).isOpenEmbedding.isCompact_iff, Set.image_univ,
    IsOpenImmersion.range_pullback_to_base_of_left]

Premises used: Set.image_univ, CategoryTheory.PreZeroHypercover.f, Topology.IsOpenEmbedding.toIsEmbedding, AlgebraicGeometry.Scheme.openCoverOfIsOpenCover, Topology.IsEmbedding.isCompact_iff, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, isCompact_univ_iff, CategoryTheory.Limits.pullback.fst, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
I : Type u_1
U : I → X.Opens
hU : IsOpenCover U
hU₁ : ∀ (i : I), IsAffineOpen (U i)
hU₂ : ∀ (i j : I), IsCompact ((↑(U i) : Set ↥X) ∩ (↑(U j) : Set ↥X))
this_1 : AffineTargetMorphismProperty.IsLocal.{u} fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u} ↥X :=
  ⋯
this : ∀ (i : (X.openCoverOfIsOpenCover U hU).I₀), IsAffine.{u} ((X.openCoverOfIsOpenCover U hU).X i)
i j : (X.openCoverOfIsOpenCover U hU).I₀
⊢ IsCompact (X := ↥X)
    (Set.range (ι := ↥((X.openCoverOfIsOpenCover U hU).X i)) ⇑((X.openCoverOfIsOpenCover U hU).f i) ∩
      Set.range (ι := ↥((X.openCoverOfIsOpenCover U hU).X j)) ⇑((X.openCoverOfIsOpenCover U hU).f j))

Tactic:
simpa using hU₂ i j
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
rw :
  autoParam
      (QuasiCompact (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
        (pullback.diagonal (terminal.from X)))
      QuasiSeparated.quasiCompact_diagonal._autoParam ↔
    QuasiCompact (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
⊢ QuasiSeparatedSpace.{u} ↥X ↔ QuasiCompact (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rw [← MorphismProperty.cancel_right_of_respectsIso @QuasiCompact _ (prodIsoPullback X X).hom,
    ← HasAffineProperty.iff_of_isAffine (f := terminal.from X) (P := @QuasiSeparated),
    quasiSeparated_iff]

Premises used: AlgebraicGeometry.quasiSeparated_iff, AlgebraicGeometry.QuasiCompact, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, prodIsoPullback, CategoryTheory.Iso.hom, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
a :
  Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
⊢ autoParam
      (QuasiCompact (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
        (pullback.diagonal (terminal.from X)))
      QuasiSeparated.quasiCompact_diagonal._autoParam ↔
    QuasiCompact (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))

Tactic:
congr!
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
a :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
a₁ :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.snd (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
⊢ Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
⊢ CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
⊢ CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.snd (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
inst rwa rwa₁ rwa₂ rwa₃ : QuasiSeparatedSpace.{u} ↥X
⊢ QuasiCompact (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rwa [← quasiSeparatedSpace_iff_quasiCompact_prod_lift]

Premises used: AlgebraicGeometry.quasiSeparatedSpace_iff_quasiCompact_prod_lift
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : QuasiSeparatedSpace.{u} ↥Y
f g : X ⟶ Y
⊢ QuasiCompact (X := equalizer f g) (equalizer.ι f g)

Tactic:
MorphismProperty.of_isPullback (P := @QuasiCompact)
    (isPullback_equalizer_prod f g).flip inferInstance

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.isPullback_equalizer_prod, inferInstance, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥Y
f g : X ⟶ Y
isCompact_univ : IsCompact.{u} (X := ↥(equalizer f g)) Set.univ
⊢ CompactSpace.{u} ↥(equalizer f g)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 : X ⟶ Y
inst : CompactSpace.{u} ↥X
inst_1 : QuasiSeparatedSpace.{u} ↥Y
f g : X ⟶ Y
⊢ IsCompact.{u} (X := ↥(equalizer f g)) Set.univ

Tactic:
simpa using QuasiCompact.isCompact_preimage (f := equalizer.ι f g) _ isOpen_univ isCompact_univ

Premises used: AlgebraicGeometry.QuasiCompact.isCompact_preimage, isOpen_univ, isCompact_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
i : 𝒰.I₀
dsimp :
  IsAffine.{u}
    (PreZeroHypercover.X
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (pullback (Y :=
            Z.affineCover.X
              (i.fst (β := fun (i : Z.affineCover.I₀) ↦
                PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
                  (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover))))
            g
            (Z.affineCover.f
              (i.fst (β := fun (i : Z.affineCover.I₀) ↦
                PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
                  (Precoverage.ZeroHypercover.toPreZeroHypercover
                    (pullback g (Z.affineCover.f i)).affineCover))))).affineCover)
      (i.snd (β := fun (i : Z.affineCover.I₀) ↦
        PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
          (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover))))
⊢ IsAffine.{u} (𝒰.X i)

Tactic:
dsimp [𝒰]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
⊢ ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)

Tactic:
have (i : _) : IsAffine (𝒰.X i) := by dsimp [𝒰]; infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
apply :
  ∀
    (i :
      ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
            fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover).toPreZeroHypercover.1),
    QuasiSeparatedSpace.{u}
      ↥((Precoverage.ZeroHypercover.pullback₁ f
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
                fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
          i)
⊢ QuasiSeparated f

Tactic:
apply HasAffineProperty.of_openCover
    ((Z.affineCover.pullback₁ g).bind fun x => Scheme.affineCover _)

Premises used: AlgebraicGeometry.HasAffineProperty.of_openCover, CategoryTheory.PreZeroHypercover.X, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.bind, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
i : Z.affineCover.I₀
j :
  PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover)
⊢ QuasiSeparatedSpace.{u}
    ↥((Precoverage.ZeroHypercover.pullback₁ f
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
              fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
        (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
          PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
            ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                    ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                        (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                      i) :
                  PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
              i))
          i j))

Tactic:
@quasiSeparatedSpace_of_quasiSeparated _ _ ?_
    (HasAffineProperty.of_isPullback (.of_hasPullback _ (Z.affineCover.f i)) ‹_›) ?_

Premises used: AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
i : Z.affineCover.I₀
j :
  PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover)
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
    fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
this : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
i : Z.affineCover.I₀
j :
  PreZeroHypercover.I₀ (S := pullback g (Z.affineCover.f i))
    (Precoverage.ZeroHypercover.toPreZeroHypercover (pullback g (Z.affineCover.f i)).affineCover)
⊢ (Precoverage.ZeroHypercover.pullback₁ f
          ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind
            fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
            ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover)).X
      (Sigma.mk (β := fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
        PreZeroHypercover.I₀ (C := Scheme) (S := (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)
          ((fun (i : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
              (Precoverage.ZeroHypercover.toPreZeroHypercover (J := Scheme.precoverage IsOpenImmersion)
                  ((fun (x : (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).I₀) ↦
                      (((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover :
                        ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).OpenCover))
                    i) :
                PreZeroHypercover ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X i)))
            i))
        i j) ⟶
    pullback (f ≫ g) (Z.affineCover.f i)

Tactic:
exact pullback.map _ _ _ _ (𝟙 _) _ _ (by simp) (Category.comp_id _) ≫
      (pullbackRightPullbackFstIso g (Z.affineCover.f i) f).hom

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.pullbackRightPullbackFstIso, CategoryTheory.Category.comp_id, CategoryTheory.Limits.pullback.map, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
inst : QuasiSeparatedSpace.{u} ↥X
⊢ QuasiSeparated f

Tactic:
have : QuasiSeparated (f ≫ Y.toSpecΓ) :=
    (HasAffineProperty.iff_of_isAffine (P := @QuasiSeparated)).mpr ‹_›
  .of_comp f Y.toSpecΓ

Premises used: Iff.mpr, AlgebraicGeometry.QuasiSeparated.of_comp, AlgebraicGeometry.Scheme.toSpecΓ, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparatedSpace.{u} ↥Y
⊢ QuasiSeparated f ↔ QuasiSeparatedSpace.{u} ↥X

Tactic:
⟨fun _ ↦ quasiSeparatedSpace_of_quasiSeparated f, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
rw rw₁ : MorphismProperty.diagonal @QuasiCompact ≤ MorphismProperty.diagonal @QuasiCompact
⊢ @QuasiSeparated ≤ MorphismProperty.diagonal @QuasiCompact

Tactic:
rw [quasiSeparated_eq_diagonal_is_quasiCompact]

Premises used: AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiCompact (f ≫ g)
inst_1 : QuasiSeparated g
⊢ QuasiCompact f

Tactic:
MorphismProperty.of_postcomp _ _ g ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : CompactSpace.{u_1} ↥X
inst_1 : QuasiSeparatedSpace.{u_1} ↥Y
⊢ QuasiCompact f

Tactic:
have : QuasiCompact (f ≫ Y.toSpecΓ) := HasAffineProperty.iff_of_isAffine.mpr ‹_›
  .of_comp f Y.toSpecΓ

Premises used: Iff.mpr, AlgebraicGeometry.QuasiCompact.of_comp, AlgebraicGeometry.Scheme.toSpecΓ, AlgebraicGeometry.HasAffineProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparatedSpace.{u} ↥Y
inst_1 : CompactSpace.{u} ↥Y
⊢ QuasiCompact f ↔ CompactSpace.{u} ↥X

Tactic:
⟨fun _ ↦ QuasiCompact.compactSpace_of_compactSpace f, fun _ ↦ inferInstance⟩

Premises used: inferInstance, AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, Iff.intro