awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV_1 : IsCompact V_1.carrier
S : X.Opens
h : IsCompact S.carrier
V : (↑X.affineOpens : Type u_1)
hV : IsCompact (U ⊓ S).carrier
mpr : IsCompact (U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ IsCompact (U.carrier ∩ S.carrier ∪ U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
apply hV.union

Premises used: IsCompact.union
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV : IsCompact V_1.carrier
S : X.Opens
h : IsCompact S.carrier
V : (↑X.affineOpens : Type u_1)
⊢ IsCompact (U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
compact_open_induction_on U hU ?_ ?_

Premises used: AlgebraicGeometry.compact_open_induction_on
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV : IsCompact V_1.carrier
S : X.Opens
h : IsCompact S.carrier
V : (↑X.affineOpens : Type u_1)
mpr : IsCompact (Opens.carrier ⊥ ∩ (↑(↑V : X.Opens) : Set ↥X))
mpr₁ :
  ∀ (S : X.Opens),
    IsCompact S.carrier →
      ∀ (U : (↑X.affineOpens : Type u_1)),
        IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X)) →
          IsCompact ((S ⊔ (↑U : X.Opens)).carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ IsCompact (U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
refine compact_open_induction_on U hU ?_ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV : IsCompact V_1.carrier
S : X.Opens
h : IsCompact S.carrier
V : (↑X.affineOpens : Type u_1)
⊢ IsCompact (Opens.carrier ⊥ ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV : IsCompact V_1.carrier
S_1 : X.Opens
h : IsCompact S_1.carrier
V : (↑X.affineOpens : Type u_1)
S : X.Opens
mpr :
  IsCompact S.carrier →
    ∀ (U : (↑X.affineOpens : Type u_1)),
      IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X)) →
        IsCompact ((S ⊔ (↑U : X.Opens)).carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ IsCompact S.carrier →
    ∀ (U : (↑X.affineOpens : Type u_1)),
      IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X)) →
        IsCompact ((S ⊔ (↑U : X.Opens)).carrier ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV : IsCompact V_1.carrier
S_1 : X.Opens
h : IsCompact S_1.carrier
V : (↑X.affineOpens : Type u_1)
S : X.Opens
h_1 : IsCompact S.carrier
W : (↑X.affineOpens : Type u_1)
hW : IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
mpr : IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X) ∪ (↑(↑W : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ IsCompact ((S.carrier ∪ (↑(↑W : X.Opens) : Set ↥X)) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
rw [Set.union_inter_distrib_right]

Premises used: Set.union_inter_distrib_right
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV : IsCompact V_1.carrier
S_1 : X.Opens
h : IsCompact S_1.carrier
V : (↑X.affineOpens : Type u_1)
S : X.Opens
h_1 : IsCompact S.carrier
W : (↑X.affineOpens : Type u_1)
hW : IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
mpr : IsCompact ((↑(↑W : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X) ∪ (↑(↑W : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
apply hW.union

Premises used: IsCompact.union
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U : X.Opens
hU : IsCompact U.carrier
V_1 : X.Opens
hV : IsCompact V_1.carrier
S_1 : X.Opens
h : IsCompact S_1.carrier
V : (↑X.affineOpens : Type u_1)
S : X.Opens
h_1 : IsCompact S.carrier
W : (↑X.affineOpens : Type u_1)
hW : IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ IsCompact ((↑(↑W : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
apply H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
rw :
  (∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
        (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) ↔
    ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ (∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
        (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) ↔
    QuasiSeparatedSpace.{u} ↥X

Tactic:
rw [quasiSeparatedSpace_iff_forall_affineOpens]

Premises used: AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
mp :
  (∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
        (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) →
    ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
mpr :
  (∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))) →
    ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂]
      [IsOpenImmersion f₁] [IsOpenImmersion f₂],
      (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
        (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
⊢ (∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
        (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) ↔
    ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
      (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : (↑X.affineOpens : Type u)
g : pullback (↑U : X.Opens).ι (↑V : X.Opens).ι ⟶ X := pullback.fst (↑U : X.Opens).ι (↑V : X.Opens).ι ≫ (↑U : X.Opens).ι
mp :
  ∀
    (e :
      ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι) ≃ₜ
        (↑(Set.range (ι := ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι)) ⇑g) : 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:
have e := g.isOpenEmbedding.isEmbedding.toHomeomorph
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
      (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : (↑X.affineOpens : Type u)
g : pullback (↑U : X.Opens).ι (↑V : X.Opens).ι ⟶ X := pullback.fst (↑U : X.Opens).ι (↑V : X.Opens).ι ≫ (↑U : X.Opens).ι
e :
  ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι) ≃ₜ
    (↑(Set.range (ι := ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι)) ⇑g) : Type u)
mp :
  ∀
    (e :
      ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι) ≃ₜ
        (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : 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:
rw [IsOpenImmersion.range_pullback_to_base_of_left, Scheme.Opens.range_ι, Scheme.Opens.range_ι]
      at e

Premises used: AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left, AlgebraicGeometry.Scheme.Opens.range_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
      (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : (↑X.affineOpens : Type u)
g : pullback (↑U : X.Opens).ι (↑V : X.Opens).ι ⟶ X := pullback.fst (↑U : X.Opens).ι (↑V : X.Opens).ι ≫ (↑U : X.Opens).ι
e :
  ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι) ≃ₜ (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)
mp : CompactSpace.{u} (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
rw [isCompact_iff_compactSpace]

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
      (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : (↑X.affineOpens : Type u)
g : pullback (↑U : X.Opens).ι (↑V : X.Opens).ι ⟶ X := pullback.fst (↑U : X.Opens).ι (↑V : X.Opens).ι ≫ (↑U : X.Opens).ι
e :
  ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι) ≃ₜ (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)
⊢ CompactSpace.{u} (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)

Tactic:
@Homeomorph.compactSpace _ _ _ _ (H _ _) e

Premises used: Homeomorph.compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H :
  ∀ ⦃U₁ U₂ : Scheme.{u}⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst_1 : IsAffine U₁] [inst_2 : IsAffine U₂] [IsOpenImmersion f₁]
    [IsOpenImmersion f₂],
    (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X) (pullback f₁ f₂)
      (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯
U V : (↑X.affineOpens : Type u)
g : pullback (↑U : X.Opens).ι (↑V : X.Opens).ι ⟶ X := pullback.fst (↑U : X.Opens).ι (↑V : X.Opens).ι ≫ (↑U : X.Opens).ι
e :
  ↥(pullback (↑U : X.Opens).ι (↑V : X.Opens).ι) ≃ₜ (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)
⊢ CompactSpace.{u} (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)

Tactic:
exact @Homeomorph.compactSpace _ _ _ _ (H _ _) e

Premises used: Homeomorph.compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
mpr :
  ∀ (e : ↥(pullback f₁ f₂) ≃ₜ (↑(Set.range (ι := ↥(pullback f₁ f₂)) ⇑g) : Type u)), CompactSpace.{u} ↥(pullback f₁ f₂)
⊢ CompactSpace.{u} ↥(pullback f₁ f₂)

Tactic:
have e := g.isOpenEmbedding.isEmbedding.toHomeomorph
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ (↑(Set.range (ι := ↥(pullback f₁ f₂)) ⇑g) : Type u)
mpr :
  ∀ (e : ↥(pullback f₁ f₂) ≃ₜ (↑(Set.range (ι := ↥U₁) ⇑f₁ ∩ Set.range (ι := ↥U₂) ⇑f₂) : Type u)),
    CompactSpace.{u} ↥(pullback f₁ f₂)
⊢ CompactSpace.{u} ↥(pullback f₁ f₂)

Tactic:
rw [IsOpenImmersion.range_pullback_to_base_of_left] at e

Premises used: AlgebraicGeometry.IsOpenImmersion.range_pullback_to_base_of_left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
H : ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ (↑(Set.range (ι := ↥U₁) ⇑f₁ ∩ Set.range (ι := ↥U₂) ⇑f₂) : Type u)
⊢ ∀ (U V : (↑X.affineOpens : Type u)),
    CompactSpace.{u} (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)

Tactic:
simp_rw [isCompact_iff_compactSpace] at H

Premises used: isCompact_iff_compactSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ (↑(Set.range (ι := ↥U₁) ⇑f₁ ∩ Set.range (ι := ↥U₂) ⇑f₂) : Type u)
H :
  ∀ (U V : (↑X.affineOpens : Type u)),
    CompactSpace.{u} (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)
⊢ CompactSpace.{u} ↥(pullback f₁ f₂)

Tactic:
@Homeomorph.compactSpace _ _ _ _
        (H ⟨_, isAffineOpen_opensRange f₁⟩ ⟨_, isAffineOpen_opensRange f₂⟩) e.symm

Premises used: Homeomorph.compactSpace, Homeomorph.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
U₁ U₂ : Scheme
f₁ : U₁ ⟶ X
f₂ : U₂ ⟶ X
inst_1 : IsAffine U₁
inst_2 : IsAffine U₂
h₁ : IsOpenImmersion f₁
h₂ : IsOpenImmersion f₂
g : pullback f₁ f₂ ⟶ X := pullback.fst f₁ f₂ ≫ f₁
e : ↥(pullback f₁ f₂) ≃ₜ (↑(Set.range (ι := ↥U₁) ⇑f₁ ∩ Set.range (ι := ↥U₂) ⇑f₂) : Type u)
H :
  ∀ (U V : (↑X.affineOpens : Type u)),
    CompactSpace.{u} (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)
⊢ CompactSpace.{u} ↥(pullback f₁ f₂)

Tactic:
exact @Homeomorph.compactSpace _ _ _ _
        (H ⟨_, isAffineOpen_opensRange f₁⟩ ⟨_, isAffineOpen_opensRange f₂⟩) e.symm

Premises used: Homeomorph.compactSpace, Homeomorph.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), QuasiSeparated x_2 ↔ MorphismProperty.diagonal (@QuasiCompact) x_2
⊢ @QuasiSeparated = MorphismProperty.diagonal @QuasiCompact

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ QuasiSeparated x_2 ↔ MorphismProperty.diagonal (@QuasiCompact) x_2

Tactic:
quasiSeparated_iff _

Premises used: CategoryTheory.MorphismProperty.diagonal, AlgebraicGeometry.quasiSeparated_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ QuasiSeparated x_2 ↔ MorphismProperty.diagonal (@QuasiCompact) x_2

Tactic:
exact quasiSeparated_iff _

Premises used: AlgebraicGeometry.quasiSeparated_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
H :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y) [inst : IsAffine Y],
    AffineTargetMorphismProperty.diagonal
        (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X) f ↔
      QuasiSeparatedSpace.{u_1} ↥X
⊢ (AffineTargetMorphismProperty.diagonal fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      CompactSpace.{u_1} ↥X) =
    fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ QuasiSeparatedSpace.{u_1} ↥X

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : IsAffine Y_1
⊢ AffineTargetMorphismProperty.diagonal
      (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X) f_1 ↔
    QuasiSeparatedSpace.{u_1} ↥X_1

Tactic:
quasiCompact_affineProperty_iff_quasiSeparatedSpace _

Premises used: AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
inst : IsAffine Y_1
⊢ AffineTargetMorphismProperty.diagonal
      (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X) f_1 ↔
    QuasiSeparatedSpace.{u_1} ↥X_1

Tactic:
exact quasiCompact_affineProperty_iff_quasiSeparatedSpace _

Premises used: AlgebraicGeometry.quasiCompact_affineProperty_iff_quasiSeparatedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderComposition @QuasiSeparated

Tactic:
quasiSeparated_eq_diagonal_is_quasiCompact.symm ▸ inferInstance

Premises used: AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact, Eq.rec, inferInstance, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderBaseChange @QuasiSeparated

Tactic:
quasiSeparated_eq_diagonal_is_quasiCompact.symm ▸ inferInstance

Premises used: AlgebraicGeometry.quasiSeparated_eq_diagonal_is_quasiCompact, Eq.rec, inferInstance, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
g : Y ⟶ Z
inst : QuasiSeparated f
inst_1 : QuasiSeparated g
⊢ QuasiSeparated (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ f g inferInstance inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X : Scheme
⊢ QuasiSeparatedSpace.{u_1} ↥X ↔ QuasiSeparated (Y := ⊤_ Scheme) (terminal.from X)

Tactic:
(HasAffineProperty.iff_of_isAffine (P := @QuasiSeparated)).symm

Premises used: AlgebraicGeometry.HasAffineProperty.iff_of_isAffine, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : QuasiSeparated g
⊢ QuasiSeparated (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.QuasiSeparated
Goal:
X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : QuasiSeparated f
⊢ QuasiSeparated (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.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
V : Y.Opens
inst : QuasiSeparated f
⊢ QuasiSeparated (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y Z : Scheme
f_1 f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : QuasiSeparated f
⊢ QuasiSeparated (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparatedSpace.{u} ↥Y
inst : QuasiSeparated f
rw :
  ∀ (hY : QuasiSeparated (Y := ⊤_ Scheme) (terminal.from Y)) [QuasiSeparated f],
    QuasiSeparated (Y := ⊤_ Scheme) (terminal.from X)
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
rw [quasiSeparatedSpace_iff_quasiSeparated] at hY ⊢

Premises used: AlgebraicGeometry.quasiSeparatedSpace_iff_quasiSeparated
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (Y := ⊤_ Scheme) (terminal.from Y)
inst : QuasiSeparated f
rw : QuasiSeparated (Y := ⊤_ Scheme) (f ≫ terminal.from Y)
⊢ QuasiSeparated (Y := ⊤_ Scheme) (terminal.from X)

Tactic:
rw [← terminalIsTerminal.hom_ext (f ≫ terminal.from Y) (terminal.from X)]

Premises used: CategoryTheory.Limits.terminal.from, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.IsTerminal.hom_ext, CategoryTheory.Limits.terminalIsTerminal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (Y := ⊤_ Scheme) (terminal.from Y)
inst : QuasiSeparated f
⊢ QuasiSeparated (Y := ⊤_ Scheme) (f ≫ terminal.from Y)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
U : Y.Opens
hU : IsQuasiSeparated (↑U : Set ↥Y)
⊢ QuasiSeparatedSpace.{u} ↥(↑U : Scheme)

Tactic:
have : QuasiSeparatedSpace U := (isQuasiSeparated_iff_quasiSeparatedSpace _ U.2).mp hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
U : Y.Opens
hU : IsQuasiSeparated (↑U : Set ↥Y)
this : QuasiSeparatedSpace.{u} ↥(↑U : Scheme)
⊢ IsQuasiSeparated (↑(f ⁻¹ᵁ U) : Set ↥X)

Tactic:
(isQuasiSeparated_iff_quasiSeparatedSpace _ (f ⁻¹ᵁ U).2).mpr
    (quasiSeparatedSpace_of_quasiSeparated (f ∣_ U))

Premises used: Iff.mpr, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', isQuasiSeparated_iff_quasiSeparatedSpace, AlgebraicGeometry.morphismRestrict, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
U : Y.Opens
hU : IsQuasiSeparated (↑U : Set ↥Y)
this : QuasiSeparatedSpace.{u} ↥(↑U : Scheme)
⊢ IsQuasiSeparated (↑(f ⁻¹ᵁ U) : Set ↥X)

Tactic:
exact (isQuasiSeparated_iff_quasiSeparatedSpace _ (f ⁻¹ᵁ U).2).mpr
    (quasiSeparatedSpace_of_quasiSeparated (f ∣_ U))

Premises used: Iff.mpr, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', isQuasiSeparated_iff_quasiSeparatedSpace, AlgebraicGeometry.morphismRestrict, CategoryTheory.Functor.obj
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
Goal:
X_1 Y Z : Scheme
f : X_1 ⟶ Y
X : Scheme
inst : IsAffine X
⊢ QuasiSeparatedSpace.{u_1} ↥X

Tactic:
(quasiSeparatedSpace_congr X.isoSpec.hom.homeomorph).2 PrimeSpectrum.instQuasiSeparatedSpace

Premises used: Iff.mpr, PrimeSpectrum.instQuasiSeparatedSpace, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Scheme.Hom.homeomorph, quasiSeparatedSpace_congr, CategoryTheory.Iso.hom