awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      CompactSpace.{u_1} ↥X).RespectsIso
have respectsIso : ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥X
Tactic: apply AffineTargetMorphismProperty.respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
respectsIso :
  ∀ {X Y Z : Scheme.{u_1}} (e : X ≅ Y) (f : Y ⟶ Z) [IsAffine Z], CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥X
⊢ (AffineTargetMorphismProperty.toProperty fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
      CompactSpace.{u_1} ↥X).RespectsIso
have respectsIso₁ : ∀ {X Y Z : Scheme.{u_1}} (e : Y ≅ Z) (f : X ⟶ Y) [IsAffine Y], CompactSpace.{u_1} ↥X → CompactSpace.{u_1} ↥X
Tactic: apply AffineTargetMorphismProperty.respectsIso_mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
inst : IsAffine Y
f : X ⟶ Y
r : (↑Γ(Y, ⊤) : Type u_1)
H : CompactSpace.{u_1} ↥X
⊢ CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen r) : Scheme)
have to_basicOpen : CompactSpace.{u_1}
  ↥(↑(X.basicOpen (U := f ⁻¹ᵁ ⊤)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (X := Γ(Y, ⊤)) (Scheme.Hom.app f ⊤) :
              (a : (↑Γ(Y, ⊤) : Type u_1)) → (↑Γ(X, f ⁻¹ᵁ ⊤) : Type u_1))
            r)) :
      Scheme)
Tactic: rw [Scheme.preimage_basicOpen f r]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS : Eq (α := Ideal (↑Γ(Y, ⊤) : Type u_1)) (Ideal.span (↑S : Set (↑Γ(Y, ⊤) : Type u_1))) ⊤
hS' : ∀ (r : ↥S), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
⊢ CompactSpace.{u_1} ↥X
have hS₁ : Eq.{u_1 + 1} (α := Y.Opens)
  (⨆ (f : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)), Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⊤
Tactic: rw [← (isAffineOpen_top _).iSup_basicOpen_eq_self_iff] at hS
Cleared hypotheses: hS, hS'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
H : IsAffine Y
f : X ⟶ Y
S : Finset (↑Γ(Y, ⊤) : Type u_1)
hS :
  Eq.{u_1 + 1} (α := Y.Opens)
    (⨆ (f : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)), Y.basicOpen (↑f : (↑Γ(Y, ⊤) : Type u_1))) ⊤
hS' : ∀ (r : ↥S), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ Y.basicOpen (↑r : (↑Γ(Y, ⊤) : Type u_1))) : Scheme)
⊢ CompactSpace.{u_1} ↥X
have of_basicOpenCover : IsCompact.{u_1} (X := ↥X)
  (⋃ (i : (↑(↑S : Set (↑Γ(Y, ⊤) : Type u_1)) : Type u_1)),
    Opens.carrier ((Opens.map f.base).1 (Y.basicOpen (↑i : (↑Γ(Y, ⊤) : Type u_1)))))
Tactic: rw [← isCompact_univ_iff, ← Opens.coe_top, ← f.preimage_top, ← hS, Scheme.Hom.preimage_iSup,
        Opens.iSup_mk, Opens.coe_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ @QuasiCompact = targetAffineLocally fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X
have h : ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
  QuasiCompact f ↔
    targetAffineLocally (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X) f
Tactic: ext X Y f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ QuasiCompact f ↔
    targetAffineLocally (fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ CompactSpace.{u_1} ↥X) f
have h : (∀ (U : Y.Opens), IsAffineOpen U → CompactSpace.{u_1} (↑(↑(f ⁻¹ᵁ U) : Set ↥X) : Type u_1)) ↔
  ∀ (a : Y.Opens) (b : a ∈ Y.affineOpens), CompactSpace.{u_1} ↥(↑(f ⁻¹ᵁ a) : Scheme)
Tactic: simp only [quasiCompact_iff_forall_isAffineOpen, isCompact_iff_compactSpace,
      targetAffineLocally, Subtype.forall]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
⊢ CompactSpace.{u_1} ↥X ↔ QuasiCompact (Y := ⊤_ Scheme) (terminal.from X)
have rw : CompactSpace.{u_1} ↥X ↔ CompactSpace.{u_1} ↥X
Tactic: rw [HasAffineProperty.iff_of_isAffine (P := @QuasiCompact)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
inst_1 : CompactSpace.{u} ↥Y
⊢ CompactSpace.{u} ↥X
have isCompact_univ : IsCompact.{u} (X := ↥X) Set.univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
⊢ MorphismProperty.IsStableUnderBaseChange @QuasiCompact
have hP' : AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X
Tactic: apply HasAffineProperty.isStableUnderBaseChange
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
⊢ AffineTargetMorphismProperty.IsStableUnderBaseChange.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
    CompactSpace.{u_1} ↥X
have hP' : ∀ ⦃X Y S : Scheme.{u_1}⦄ [IsAffine S] [IsAffine X] (f : X ⟶ S) (g : Y ⟶ S),
  CompactSpace.{u_1} ↥Y → CompactSpace.{u_1} ↥(pullback f g)
Tactic: apply AffineTargetMorphismProperty.IsStableUnderBaseChange.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ Finite.{u_1 + 1} 𝒰.I₀
have dsimp : Finite.{u_1 + 1} Y.affineCover.finiteSubcover.I₀
Tactic: dsimp [𝒰]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
⊢ CompactSpace.{u_1} ↥(pullback f g)
have this₁ : Finite.{u_1 + 1} 𝒰.I₀
Tactic: have : Finite 𝒰.I₀ := by dsimp [𝒰]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this_1 : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite.{u_1 + 1} 𝒰.I₀
i : 𝒰.I₀
⊢ CompactSpace.{u_1} ↥(𝒰.X i)
have dsimp : CompactSpace.{u_1}
  ↥(pullback (Y := Y.affineCover.X (Scheme.Cover.idx Y.affineCover (↑i : ↥Y))) f
      (Y.affineCover.f (Scheme.Cover.idx Y.affineCover (↑i : ↥Y)) ≫ g))
Tactic: dsimp [𝒰]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
this_1 : AffineTargetMorphismProperty.IsLocal.{u_1} fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦
  CompactSpace.{u_1} ↥X :=
  ⋯
X Y S : Scheme
inst : IsAffine S
inst_1 : IsAffine X
f : X ⟶ S
g : Y ⟶ S
h : CompactSpace.{u_1} ↥Y
𝒰 : (pullback f g).OpenCover := Scheme.Pullback.openCoverOfRight Y.affineCover.finiteSubcover f g
this : Finite.{u_1 + 1} 𝒰.I₀
⊢ CompactSpace.{u_1} ↥(pullback f g)
have this₁ : ∀ (i : 𝒰.I₀), CompactSpace.{u_1} ↥(𝒰.X i)
Tactic: have : ∀ i, CompactSpace (𝒰.X i) := by intro i; dsimp [𝒰]; infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
⊢ IsCompact (↑U : Set ↥X) ↔ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
have refine : (∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)), Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f) ↔
  ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
Tactic: refine isCompact_iff_compactSpace.trans ((compactSpace_iff_exists (X := U)).trans ?_)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
⊢ (∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)),
      Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f) ↔
    ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
have refine : (∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)) →
  ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ X) (hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)),
    ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)), Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f
Tactic: refine ⟨fun ⟨R, f, hf⟩ ↦ ⟨R, f ≫ U.ι, by simp [hf.range_comp]⟩, fun ⟨R, f, hf⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
⊢ ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ (↑U : Scheme)), Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑f
have refine : Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑(IsOpenImmersion.lift U.ι f sorry)
Tactic: refine ⟨R, IsOpenImmersion.lift U.ι f (by simp [hf]), ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
⊢ Function.Surjective (α := ↥(Spec R)) (β := ↥(↑U : Scheme)) ⇑(IsOpenImmersion.lift U.ι f ⋯)
have rw : Eq (α := Set ↥(↑U : Scheme)) (Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f sorry)) Set.univ
Tactic: rw [← Set.range_eq_univ]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
⊢ Eq (α := Set ↥(↑U : Scheme)) (Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯)) Set.univ
have a : Eq.{u + 1} (α := Set ↥X)
  ((fun (x : Set ↥(↑U : Scheme)) ↦ (⇑U.ι '' x : Set ↥X)) (Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f sorry)))
  ((fun (x : Set ↥(↑U : Scheme)) ↦ (⇑U.ι '' x : Set ↥X)) Set.univ)
Tactic: apply show Function.Injective (U.ι '' ·) from Set.image_val_injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
⊢ Eq.{u + 1} (α := Set ↥X)
    ((fun (x : Set ↥(↑U : Scheme)) ↦ (⇑U.ι '' x : Set ↥X)) (Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯)))
    ((fun (x : Set ↥(↑U : Scheme)) ↦ (⇑U.ι '' x : Set ↥X)) Set.univ)
have a : (fun (a : ↥(↑U : Scheme)) ↦ U.ι a) '' Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f sorry) = (↑U : Set ↥X)
Tactic: simp only [Set.image_univ, Scheme.Opens.range_ι]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
⊢ (fun (a : ↥(↑U : Scheme)) ↦ U.ι a) '' Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯) = (↑U : Set ↥X)
have a : Set.range (ι := ↥(Spec R)) ((fun (a : ↥(↑U : Scheme)) ↦ U.ι a) ∘ ⇑(IsOpenImmersion.lift U.ι f sorry)) = (↑U : Set ↥X)
Tactic: rwa [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsOpenImmersion.lift_fac]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
a : Set.range (ι := ↥(Spec R)) ((fun (a : ↥(↑U : Scheme)) ↦ U.ι a) ∘ ⇑(IsOpenImmersion.lift U.ι f ⋯)) = (↑U : Set ↥X)
⊢ (fun (a : ↥(↑U : Scheme)) ↦ U.ι a) '' Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯) = (↑U : Set ↥X)
have a₁ : Set.range (ι := ↥(Spec R))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
          ((IsOpenImmersion.lift U.ι f sorry).base ≫ U.ι.base)) :
      (a : ↥(Spec R)) → ↥X) =
  (↑U : Set ↥X)
Tactic: rwa [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsOpenImmersion.lift_fac]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
U : X.Opens
h : ∃ (R : CommRingCat.{u}) (f : Spec R ⟶ X), Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range (ι := ↥(Spec R)) ⇑f = (↑U : Set ↥X)
a : Set.range (ι := ↥(Spec R)) ((fun (a : ↥(↑U : Scheme)) ↦ U.ι a) ∘ ⇑(IsOpenImmersion.lift U.ι f ⋯)) = (↑U : Set ↥X)
a₁ :
  Set.range (ι := ↥(Spec R))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            ((IsOpenImmersion.lift U.ι f ⋯).base ≫ U.ι.base)) :
        (a : ↥(Spec R)) → ↥X) =
    (↑U : Set ↥X)
⊢ (fun (a : ↥(↑U : Scheme)) ↦ U.ι a) '' Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f ⋯) = (↑U : Set ↥X)
have a₂ : Set.range (ι := ↥(Spec R)) ⇑(IsOpenImmersion.lift U.ι f sorry ≫ U.ι) = (↑U : Set ↥X)
Tactic: rwa [← Set.range_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base, IsOpenImmersion.lift_fac]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f ↔ SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f
have refine : ∀ (H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
Tactic: refine ⟨fun h ↦ h.specializingMap, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
have inr : ∀
  (this :
    ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f)
      (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f)
  (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f)
        (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
have wlog : ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f)
  (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
⊢ topologically (@IsClosedMap) f
have inr : ∀ (i : Y.affineCover.toPreZeroHypercover.1),
  topologically @IsClosedMap (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically @IsClosedMap) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ topologically @IsClosedMap (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
have x : QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
  (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
    (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
Tactic: have _ : QuasiCompact (Y.affineCover.pullbackHom f i) := MorphismProperty.pullback_snd _ _ ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [QuasiCompact f] (H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f)
    (hY : ∃ (R : CommRingCat.{u}), Y = Spec R), IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
h :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ topologically @IsClosedMap (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
have inr : SpecializingMap (X := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)) (Y := ↥(Y.affineCover.X i))
  ⇑(Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i)
Tactic: refine this (Y.affineCover.pullbackHom f i) ?_ ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f
have obtain : ∀ (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (H : SpecializingMap (X := ↥X) (Y := ↥(Spec S)) ⇑f),
  IsClosedMap (X := ↥X) (Y := ↥(Spec S)) ⇑f
Tactic: obtain ⟨S, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, H, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
H : SpecializingMap (X := ↥X) (Y := ↥(Spec S)) ⇑f
Z : Set ↥X
hZ : IsClosed Z
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have H₁ : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
Tactic: replace H := hZ.stableUnderSpecialization.image H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X) (hZ : IsClosed Z)
      (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
      IsClosed (X := ↥(Spec S)) (⇑f '' Z))
  (hX : ¬∃ (R : CommRingCat.{u}), X = Spec R), IsClosed (X := ↥(Spec S)) (⇑f '' Z)
Tactic: wlog hX : ∃ R, X = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X) (hZ : IsClosed Z)
        (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
        IsClosed (X := ↥(Spec S)) (⇑f '' Z))
    (hX : ¬∃ (R : CommRingCat.{u}), X = Spec R), IsClosed (X := ↥(Spec S)) (⇑f '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have wlog : ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X) (hZ : IsClosed Z)
  (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
  IsClosed (X := ↥(Spec S)) (⇑f '' Z)
Tactic: wlog hX : ∃ R, X = Spec R
Cleared hypotheses: X, S, f, inst, Z, hZ, H
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (goal)
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
this :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X) (hZ : IsClosed Z)
    (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    IsClosed (X := ↥(Spec S)) (⇑f '' Z)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have inr : ∀ (R : CommRingCat.{u}) (g : Spec R ⟶ X) (hg : Function.Surjective (α := ↥(Spec R)) (β := ↥X) ⇑g),
  IsClosed (X := ↥(Spec S)) (⇑f '' Z)
Tactic: obtain ⟨R, g, hg⟩ := compactSpace_iff_exists.mp (QuasiCompact.compactSpace_of_compactSpace f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact (hypothesis)
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
this :
  ∀ {X : Scheme.{u}} (S : CommRingCat.{u}) (f : X ⟶ Spec S) [QuasiCompact f] (Z : Set ↥X) (hZ : IsClosed Z)
    (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R : CommRingCat.{u}), X = Spec R),
    IsClosed (X := ↥(Spec S)) (⇑f '' Z)
hX : ¬∃ (R : CommRingCat.{u}), X = Spec R
R : CommRingCat
g : Spec R ⟶ X
hg : Function.Surjective (α := ↥(Spec R)) (β := ↥X) ⇑g
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)
have inst : QuasiCompact (g ≫ f)
Tactic: have inst : QuasiCompact (g ≫ f) := HasAffineProperty.iff_of_isAffine.mpr (by infer_instance)