awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
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
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
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)
⊢ topologically (@IsClosedMap) f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically @IsClosedMap) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
⊢ 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 _ _ ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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)

Tactic:
this (Y.affineCover.pullbackHom f i) ?_ ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, AlgebraicGeometry.topologically, Exists.intro, AlgebraicGeometry.Scheme.affineCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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)
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)
⊢ 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:
refine this (Y.affineCover.pullbackHom f i) ?_ ⟨_, rfl⟩

Premises used: AlgebraicGeometry.Scheme.Cover.pullbackHom, Exists.intro, AlgebraicGeometry.Scheme.affineCover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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)
⊢ 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:
IsZariskiLocalAtTarget.of_isPullback
      (P := topologically @SpecializingMap) (.of_hasPullback _ _) H

Premises used: AlgebraicGeometry.topologically, AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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)
⊢ 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:
exact IsZariskiLocalAtTarget.of_isPullback
      (P := topologically @SpecializingMap) (.of_hasPullback _ _) H

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X Y : Scheme
f : X ⟶ Y
inst : QuasiCompact f
H : SpecializingMap (X := ↥X) (Y := ↥Y) ⇑f
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
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
⊢ IsClosedMap (X := ↥X) (Y := ↥Y) ⇑f

Tactic:
obtain ⟨S, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
⊢ StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)

Tactic:
replace H := hZ.stableUnderSpecialization.image H
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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)
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)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)

Tactic:
wlog hX : ∃ R, X = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
inr :
  ∀ (R : CommRingCat.{u}) (g : Spec R ⟶ X) (hg : Function.Surjective (α := ↥(Spec R)) (β := ↥X) ⇑g),
    IsClosed (X := ↥(Spec S)) (⇑f '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)

Tactic:
obtain ⟨R, g, hg⟩ := compactSpace_iff_exists.mp (QuasiCompact.compactSpace_of_compactSpace f)

Premises used: AlgebraicGeometry.QuasiCompact.compactSpace_of_compactSpace, AlgebraicGeometry.compactSpace_iff_exists, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
⊢ CompactSpace.{u} ↥(Spec R)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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
⊢ QuasiCompact (g ≫ f)

Tactic:
have inst : QuasiCompact (g ≫ f) := HasAffineProperty.iff_of_isAffine.mpr (by infer_instance)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : 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
inst : QuasiCompact (g ≫ f)
⊢ ∀ (H : StableUnderSpecialization (X := ↥(Spec S)) (Set.image (α := ↥(Spec R)) (⇑(g ≫ f)) (⇑g ⁻¹' Z)))
    (hX : ∃ (R_1 : CommRingCat.{u}), Spec R = Spec R_1),
    IsClosed (X := ↥(Spec S)) (Set.image (α := ↥(Spec R)) (⇑(g ≫ f)) (⇑g ⁻¹' Z))

Tactic:
have := this _ (g ≫ f) (g ⁻¹' Z) (hZ.preimage g.continuous)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
this_1 :
  ∀ {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
inst : QuasiCompact (g ≫ f)
this :
  ∀ (H : StableUnderSpecialization (X := ↥(Spec S)) (Set.image (α := ↥(Spec R)) (⇑(g ≫ f)) (⇑g ⁻¹' Z)))
    (hX : ∃ (R_1 : CommRingCat.{u}), Spec R = Spec R_1),
    IsClosed (X := ↥(Spec S)) (Set.image (α := ↥(Spec R)) (⇑(g ≫ f)) (⇑g ⁻¹' Z))
⊢ ∀ (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R_1 : CommRingCat.{u}), Spec R = Spec R_1),
    IsClosed (X := ↥(Spec S)) (⇑f '' Z)

Tactic:
simp_rw [Scheme.Hom.comp_base, TopCat.comp_app, ← Set.image_image,
      Set.image_preimage_eq _ hg] at this

Premises used: Set.image_image, Set.image_preimage_eq, TopCat.comp_app, AlgebraicGeometry.Scheme.Hom.comp_base
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
this_1 :
  ∀ {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
inst : QuasiCompact (g ≫ f)
this :
  ∀ (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R_1 : CommRingCat.{u}), Spec R = Spec R_1),
    IsClosed (X := ↥(Spec S)) (⇑f '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)

Tactic:
this H ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
S : CommRingCat
f : X ⟶ Spec S
inst_1 : QuasiCompact f
Z : Set ↥X
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
this_1 :
  ∀ {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
inst : QuasiCompact (g ≫ f)
this :
  ∀ (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)) (hX : ∃ (R_1 : CommRingCat.{u}), Spec R = Spec R_1),
    IsClosed (X := ↥(Spec S)) (⇑f '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)

Tactic:
exact this H ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
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)
hX : ∃ (R : CommRingCat.{u}), X = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : Spec R ⟶ Spec S) [QuasiCompact f] (Z : Set ↥(Spec R)) (hZ : IsClosed Z)
    (H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)), IsClosed (X := ↥(Spec S)) (⇑f '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)

Tactic:
obtain ⟨R, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
S R : CommRingCat
f : Spec R ⟶ Spec S
inst : QuasiCompact f
Z : Set ↥(Spec R)
hZ : IsClosed Z
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑f '' Z)
obtain :
  ∀ (φ : S ⟶ R)
    [QuasiCompact.{u} (X := Spec R) (Y := Spec S) ((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ)]
    (H :
      StableUnderSpecialization (X := ↥(Spec S))
        (⇑((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ) '' Z)),
    IsClosed (X := ↥(Spec S)) (⇑((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ) '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑f '' Z)

Tactic:
obtain ⟨φ, rfl⟩ := Spec.homEquiv.symm.surjective f

Premises used: AlgebraicGeometry.Spec.homEquiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
S R : CommRingCat
Z : Set ↥(Spec R)
hZ : IsClosed Z
φ : S ⟶ R
inst : QuasiCompact.{u} (X := Spec R) (Y := Spec S) ((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ)
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ) '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ) '' Z)

Tactic:
PrimeSpectrum.isClosed_image_of_stableUnderSpecialization φ.hom Z hZ H

Premises used: CommRingCat.Hom.hom, PrimeSpectrum.comap, PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
S R : CommRingCat
Z : Set ↥(Spec R)
hZ : IsClosed Z
φ : S ⟶ R
inst : QuasiCompact.{u} (X := Spec R) (Y := Spec S) ((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ)
H : StableUnderSpecialization (X := ↥(Spec S)) (⇑((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ) '' Z)
⊢ IsClosed (X := ↥(Spec S)) (⇑((Equiv.symm Spec.homEquiv : (a : S ⟶ R) → Spec R ⟶ Spec S) φ) '' Z)

Tactic:
exact PrimeSpectrum.isClosed_image_of_stableUnderSpecialization φ.hom Z hZ H

Premises used: CommRingCat.Hom.hom, PrimeSpectrum.isClosed_image_of_stableUnderSpecialization
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
P : X.Opens → Prop
S : X.Opens
hS : IsCompact (↑S : Set ↥X)
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
obtain :
  ∀ (s : Set (↑X.affineOpens : Type u)) (hs : s.Finite) (hS : IsCompact (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)),
    P (⨆ i ∈ s, (↑i : X.Opens))
⊢ P S

Tactic:
obtain ⟨s, hs, rfl⟩ := isCompact_iff_finite_and_eq_biUnion_affineOpens.mp hS

Premises used: Iff.mp, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
hS : IsCompact (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)
⊢ P (⨆ (i : (↑X.affineOpens : Type u)), ⨆ (_ : Membership.mem (γ := Set (↑X.affineOpens : Type u)) ∅ i), (↑i : X.Opens))

Tactic:
simpa using h₁
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
s : Set (↑X.affineOpens : Type u)
hs : s.Finite
hS : IsCompact (↑(⨆ i ∈ s, (↑i : X.Opens)) : Set ↥X)
refine :
  ∀ {x : (↑X.affineOpens : Type u)} {s : Set (↑X.affineOpens : Type u)},
    x ∉ s → ∀ (hs : s.Finite) (h₄ : P (⨆ i ∈ s, (↑i : X.Opens))), P (⨆ i ∈ insert x s, (↑i : X.Opens))
⊢ P (⨆ i ∈ s, (↑i : X.Opens))

Tactic:
refine hs.induction_on _ (by simpa using h₁) fun {x s} _ hs h₄ ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
s_1 : Set (↑X.affineOpens : Type u)
hs_1 : s_1.Finite
hS : IsCompact (↑(⨆ i ∈ s_1, (↑i : X.Opens)) : Set ↥X)
x : (↑X.affineOpens : Type u)
s : Set (↑X.affineOpens : Type u)
h : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, (↑i : X.Opens))
rw : P ((⨆ x ∈ s, (↑x : X.Opens)) ⊔ (↑x : X.Opens))
⊢ P (⨆ i ∈ insert x s, (↑i : X.Opens))

Tactic:
rw [iSup_insert, sup_comm]

Premises used: iSup_insert, sup_comm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
s_1 : Set (↑X.affineOpens : Type u)
hs_1 : s_1.Finite
hS : IsCompact (↑(⨆ i ∈ s_1, (↑i : X.Opens)) : Set ↥X)
x : (↑X.affineOpens : Type u)
s : Set (↑X.affineOpens : Type u)
h : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, (↑i : X.Opens))
⊢ Eq.{u + 1} (α := X.Opens) (⨆ x ∈ s, (↑x : X.Opens)) (⨆ i ∈ s, (↑i : X.Opens))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
P : X.Opens → Prop
h₁ : P ⊥
h₂ : ∀ (S : X.Opens), IsCompact S.carrier → ∀ (U : (↑X.affineOpens : Type u)), P S → P (S ⊔ (↑U : X.Opens))
s_1 : Set (↑X.affineOpens : Type u)
hs_1 : s_1.Finite
hS : IsCompact (↑(⨆ i ∈ s_1, (↑i : X.Opens)) : Set ↥X)
x : (↑X.affineOpens : Type u)
s : Set (↑X.affineOpens : Type u)
h : x ∉ s
hs : s.Finite
h₄ : P (⨆ i ∈ s, (↑i : X.Opens))
⊢ P ((⨆ x ∈ s, (↑x : X.Opens)) ⊔ (↑x : X.Opens))

Tactic:
exact h₂ _ (isCompact_iff_finite_and_eq_biUnion_affineOpens.mpr ⟨s, hs, by simp⟩) x h₄

Premises used: Iff.mpr, And.intro, Exists.intro, AlgebraicGeometry.isCompact_iff_finite_and_eq_biUnion_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : (↑Γ(X, U) : Type u_1)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    0
⊢ Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
      0)

Tactic:
rw [← map_zero (X.presheaf.map (homOfLE <| X.basicOpen_le f : X.basicOpen f ⟶ U).op).hom] at H

Premises used: CommRingCat.Hom.hom, Quiver.Hom.op, AlgebraicGeometry.Scheme.basicOpen_le, map_zero, CategoryTheory.Functor.map, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : (↑Γ(X, U) : Type u_1)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
      0)
obtain : ∀ (n : ℕ) (e : f ^ n * x = f ^ n * 0), ∃ (n : ℕ), f ^ n * x = 0
⊢ ∃ (n : ℕ), f ^ n * x = 0

Tactic:
obtain ⟨n, e⟩ := (hU.isLocalization_basicOpen f).exists_of_eq _ H

Premises used: IsLocalization.Away.exists_of_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x f : (↑Γ(X, U) : Type u_1)
H :
  Eq (α :=
    ToType (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (op (X.basicOpen f))))
    (TopCat.Presheaf.restrictOpen (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
      CommRingCat.carrier) x (X.basicOpen f) ⋯)
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
        (a : (↑Γ(X, U) : Type u_1)) → (↑Γ(X, X.basicOpen f) : Type u_1))
      0)
n : ℕ
e : f ^ n * x = f ^ n * 0
⊢ f ^ n * x = 0

Tactic:
simpa [mul_comm x] using e

Premises used: mul_comm