awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (goal)
Goal:
R S : CommRingCat
x : ↥(Spec S)
φ : R ⟶ S
inst : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u, u} (↑R : Type u) (↑S : Type u)
this : Algebra (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
  (Localization.AtPrime x.asIdeal) :=
  Localization.AtPrime.algebraOfLiesOver (Ideal.under (↑R : Type u) x.asIdeal) x.asIdeal
⊢ QuasiFiniteAt (Spec.map φ) x ↔
    Algebra.QuasiFinite.{u, u} (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (Localization.AtPrime x.asIdeal)
have rw : QuasiFiniteAt (Spec.map φ) x ↔
  RingHom.QuasiFinite.{u, u} (R := Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
    (S := Localization.AtPrime x.asIdeal)
    (algebraMap (Localization.AtPrime (R := (↑R : Type u)) (Ideal.under (↑R : Type u) x.asIdeal))
      (Localization.AtPrime x.asIdeal))
Tactic: rw [← RingHom.quasiFinite_algebraMap]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
hx : QuasiFiniteAt f x
⊢ IsClopen (X := ↥(fiber f (f x))) {asFiber f x}
have this : IsOpen (X := ↥(fiber f (f x))) {asFiber f x}
Tactic: have := Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber.mp ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
⊢ QuasiSeparatedSpace.{u_1} ↥X ↔
    ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have rw : (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
  ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: rw [quasiSeparatedSpace_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
⊢ (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have mp : (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) →
  ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
mp :
  (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) →
    ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have mpr : (∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))) →
  ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
H : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
have mpr : ∀ (U : X.Opens), IsCompact U.carrier → ∀ (V : X.Opens), IsCompact V.carrier → IsCompact (U ⊓ V).carrier
Tactic: suffices
      ∀ (U : X.Opens) (_ : IsCompact U.1) (V : X.Opens) (_ : IsCompact V.1),
        IsCompact (U ⊓ V).1
      by intro U V hU hU' hV hV'; exact this ⟨U, hU⟩ hU' ⟨V, hV⟩ hV'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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 : X.Opens
hV : IsCompact V.carrier
⊢ IsCompact (U ⊓ V).carrier
have mpr : IsCompact (U ⊓ ⊥).carrier
Tactic: refine compact_open_induction_on V hV ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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 : X.Opens
hV : IsCompact V.carrier
mpr : IsCompact (U ⊓ ⊥).carrier
⊢ IsCompact (U ⊓ V).carrier
have mpr₁ : ∀ (S : X.Opens),
  IsCompact S.carrier →
    ∀ (U_1 : (↑X.affineOpens : Type u_1)), IsCompact (U ⊓ S).carrier → IsCompact (U ⊓ (S ⊔ (↑U_1 : X.Opens))).carrier
Tactic: refine compact_open_induction_on V hV ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
⊢ IsCompact (U.carrier ∩ (S.carrier ∪ (↑(↑V : X.Opens) : Set ↥X)))
have mpr : IsCompact (U.carrier ∩ S.carrier ∪ U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: rw [Set.inter_union_distrib_left]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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
⊢ IsCompact (U.carrier ∩ S.carrier ∪ U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
have mpr : IsCompact (U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: apply hV.union
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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))
have mpr : IsCompact (Opens.carrier ⊥ ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: refine compact_open_induction_on U hU ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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))
⊢ IsCompact (U.carrier ∩ (↑(↑V : X.Opens) : Set ↥X))
have 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))
Tactic: refine compact_open_induction_on U hU ?_ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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 ((S.carrier ∪ (↑(↑W : X.Opens) : Set ↥X)) ∩ (↑(↑V : X.Opens) : Set ↥X))
have mpr : IsCompact (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X) ∪ (↑(↑W : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: rw [Set.union_inter_distrib_right]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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 (S.carrier ∩ (↑(↑V : X.Opens) : Set ↥X) ∪ (↑(↑W : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have mpr : IsCompact ((↑(↑W : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: apply hW.union
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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
have 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) sorry) ↔
  ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: rw [quasiSeparatedSpace_iff_forall_affineOpens]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃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))
have 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) sorry) →
  ∀ (U V : (↑X.affineOpens : Type u)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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))
⊢ (∀ ⦃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))
have 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) sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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).ι
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have 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))
Tactic: have e := g.isOpenEmbedding.isEmbedding.toHomeomorph
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have 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))
Tactic: rw [IsOpenImmersion.range_pullback_to_base_of_left, Scheme.Opens.range_ι, Scheme.Opens.range_ι]
      at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have mp : CompactSpace.{u} (↑((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) : Type u)
Tactic: rw [isCompact_iff_compactSpace]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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₁
⊢ CompactSpace.{u} ↥(pullback f₁ f₂)
have mpr : ∀ (e : ↥(pullback f₁ f₂) ≃ₜ (↑(Set.range (ι := ↥(pullback f₁ f₂)) ⇑g) : Type u)), CompactSpace.{u} ↥(pullback f₁ f₂)
Tactic: have e := g.isOpenEmbedding.isEmbedding.toHomeomorph
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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)
⊢ CompactSpace.{u} ↥(pullback f₁ f₂)
have mpr : ∀ (e : ↥(pullback f₁ f₂) ≃ₜ (↑(Set.range (ι := ↥U₁) ⇑f₁ ∩ Set.range (ι := ↥U₂) ⇑f₂) : Type u)),
  CompactSpace.{u} ↥(pullback f₁ f₂)
Tactic: rw [IsOpenImmersion.range_pullback_to_base_of_left] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (hypothesis)
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)
⊢ CompactSpace.{u} ↥(pullback f₁ f₂)
have H₁ : ∀ (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
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
⊢ @QuasiSeparated = MorphismProperty.diagonal @QuasiCompact
have h : ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1), QuasiSeparated x_2 ↔ MorphismProperty.diagonal (@QuasiCompact) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y Z : Scheme
f : X ⟶ Y
⊢ (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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparatedSpace.{u} ↥Y
inst : QuasiSeparated f
⊢ QuasiSeparatedSpace.{u} ↥X
have rw : ∀ (hY : QuasiSeparated (Y := ⊤_ Scheme) (terminal.from Y)) [QuasiSeparated f],
  QuasiSeparated (Y := ⊤_ Scheme) (terminal.from X)
Tactic: rw [quasiSeparatedSpace_iff_quasiSeparated] at hY ⊢
Cleared hypotheses: hY, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (Y := ⊤_ Scheme) (terminal.from Y)
inst : QuasiSeparated f
⊢ QuasiSeparated (Y := ⊤_ Scheme) (terminal.from X)
have rw : QuasiSeparated (Y := ⊤_ Scheme) (f ≫ terminal.from Y)
Tactic: rw [← terminalIsTerminal.hom_ext (f ≫ terminal.from Y) (terminal.from X)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiSeparated f
U : Y.Opens
hU : IsQuasiSeparated (↑U : Set ↥Y)
⊢ IsQuasiSeparated (↑(f ⁻¹ᵁ U) : Set ↥X)
have this : QuasiSeparatedSpace.{u} ↥(↑U : Scheme)
Tactic: have : QuasiSeparatedSpace U := (isQuasiSeparated_iff_quasiSeparatedSpace _ U.2).mp hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ IsQuasiSeparated (↑U : Set ↥X)
have rw : QuasiSeparatedSpace.{u} (↑(↑U : Set ↥X) : Type u)
Tactic: rw [isQuasiSeparated_iff_quasiSeparatedSpace]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
rw : QuasiSeparatedSpace.{u} (↑(↑U : Set ↥X) : Type u)
⊢ IsQuasiSeparated (↑U : Set ↥X)
have hs : IsOpen (↑U : Set ↥X)
Tactic: rw [isQuasiSeparated_iff_quasiSeparatedSpace]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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 :=
  ⋯
⊢ QuasiSeparatedSpace.{u} ↥X
have rw : AffineTargetMorphismProperty.diagonal (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X)
  X.toSpecΓ
Tactic: rw [← quasiCompact_affineProperty_iff_quasiSeparatedSpace X.toSpecΓ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (hypothesis)
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 :=
  ⋯
⊢ AffineTargetMorphismProperty.diagonal (fun (X x : Scheme.{u}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u} ↥X)
    X.toSpecΓ
have this₁ : ∀ (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₁
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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Γ
have refine : ∀ (i j : (X.openCoverOfIsOpenCover U hU).I₀),
  CompactSpace.{u} ↥(pullback ((X.openCoverOfIsOpenCover U hU).f i) ((X.openCoverOfIsOpenCover U hU).f j))
Tactic: refine AffineTargetMorphismProperty.diagonal_of_openCover_source _
    (Scheme.openCoverOfIsOpenCover _ _ hU) fun i j ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
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₀
⊢ CompactSpace.{u} ↥(pullback ((X.openCoverOfIsOpenCover U hU).f i) ((X.openCoverOfIsOpenCover U hU).f j))
have 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))
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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated (goal)
Goal:
X : Scheme
⊢ QuasiSeparatedSpace.{u} ↥X ↔ QuasiCompact (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X))
have 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))
Tactic: rw [← MorphismProperty.cancel_right_of_respectsIso @QuasiCompact _ (prodIsoPullback X X).hom,
    ← HasAffineProperty.iff_of_isAffine (f := terminal.from X) (P := @QuasiSeparated),
    quasiSeparated_iff]