awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [hf : LocallyOfFinitePresentation f] [QuasiCompact f] {s : Set ↥X}
    (hs : IsLocallyConstructible s) (hY : ∃ (R : CommRingCat.{u}), Y = Spec R),
    IsLocallyConstructible (X := ↥Y) (⇑f '' s)
hY : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.I₀
inst_2 :
  LocallyOfFinitePresentation (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
inst :
  QuasiCompact (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
    (Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
      (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
e_1 : (↑(↑(opensRange (Y.affineCover.f i)) : Set ↥Y) : Type u) = ↥(↑(opensRange (Y.affineCover.f i)) : Scheme)
⊢ ⇑f '' s ∩ (↑(opensRange (Y.affineCover.f i)) : Set ↥Y) =
    (⇑(TopCat.Hom.hom f.base) : (a : ↥X) → ↥Y) ''
      (s ∩
        Set.range (ι := ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i))
          (⇑(TopCat.Hom.hom ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i).base) :
            (a : ↥((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)) → ↥X))

Tactic:
simp [IsOpenImmersion.range_pullbackFst, Set.image_inter_preimage]

Premises used: Set.image_inter_preimage, AlgebraicGeometry.IsOpenImmersion.range_pullbackFst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
s : Set ↥X
hs : IsLocallyConstructible s
hY : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [hf : LocallyOfFinitePresentation f] [QuasiCompact f],
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
⊢ IsLocallyConstructible (X := ↥Y) (⇑f '' s)

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
        [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
        IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s))
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
wlog :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
⊢ CompactSpace.{u} ↥X

Tactic:
have inst : CompactSpace X := HasAffineProperty.iff_of_isAffine.mp ‹QuasiCompact f›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
inr : IsLocallyConstructible.{u} (X := ↥(Spec R)) (⋃ (i : 𝒰.I₀), ⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)

Tactic:
rw [← 𝒰.isOpenCover_opensRange.iUnion_inter s, Set.image_iUnion]

Premises used: AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, Set.image_iUnion, TopologicalSpace.IsOpenCover.iUnion_inter
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ IsLocallyConstructible.{u} (X := ↥(Spec R)) (⋃ (i : 𝒰.I₀), ⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))

Tactic:
.iUnion fun i ↦ ?_

Premises used: Topology.IsLocallyConstructible.iUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
inr : ∀ (i : 𝒰.I₀), IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
⊢ IsLocallyConstructible.{u} (X := ↥(Spec R)) (⋃ (i : 𝒰.I₀), ⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))

Tactic:
refine .iUnion fun i ↦ ?_
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
⊢ QuasiCompact (𝒰.f i ≫ f)

Tactic:
have inst : QuasiCompact (𝒰.f i ≫ f) :=
      HasAffineProperty.iff_of_isAffine.mpr (inferInstanceAs (CompactSpace (Spec _)))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst_2 : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
inst : QuasiCompact (𝒰.f i ≫ f)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i ≫ f)) (⇑(𝒰.f i) ⁻¹' s))

Tactic:
this (hs.preimage_of_isOpenEmbedding (𝒰.f i).isOpenEmbedding) _ (𝒰.f i ≫ f) ⟨_, rfl⟩

Premises used: Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
this :
  ∀ {X : Scheme.{u}} {s : Set ↥X} (hs : IsLocallyConstructible s) (R : CommRingCat.{u}) (f : X ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f] (hX : ∃ (S : CommRingCat.{u}), X = Spec S),
    IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
hX : ¬∃ (S : CommRingCat.{u}), X = Spec S
inst_2 : CompactSpace.{u} ↥X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
inst : QuasiCompact (𝒰.f i ≫ f)
h :
  Eq (α := Set ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))
    (Set.image (α := ↥(𝒰.X i)) (⇑(𝒰.f i ≫ f)) (⇑(𝒰.f i) ⁻¹' s))
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' (s ∩ (↑(opensRange (𝒰.f i)) : Set ↥X)))

Tactic:
convert! this (hs.preimage_of_isOpenEmbedding (𝒰.f i).isOpenEmbedding) _ (𝒰.f i ≫ f) ⟨_, rfl⟩

Premises used: Topology.IsLocallyConstructible.preimage_of_isOpenEmbedding, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Exists.intro, CategoryTheory.CategoryStruct.comp, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X : Scheme
s : Set ↥X
hs : IsLocallyConstructible s
R : CommRingCat
f : X ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
hX : ∃ (S : CommRingCat.{u}), X = Spec S
obtain :
  ∀ (S : CommRingCat.{u}) {s : Set ↥(Spec S)} (hs : IsLocallyConstructible s) (f : Spec S ⟶ Spec R)
    [hf : LocallyOfFinitePresentation f] [QuasiCompact f], IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
f : Spec S ⟶ Spec R
hf : LocallyOfFinitePresentation f
inst : QuasiCompact f
obtain :
  ∀ (φ : R ⟶ S) [hf : LocallyOfFinitePresentation (Spec.map φ)] [QuasiCompact (Spec.map φ)],
    IsLocallyConstructible (X := ↥(Spec R)) (⇑(Spec.map φ) '' s)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑f '' s)

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
φ : R ⟶ S
hf : LocallyOfFinitePresentation (Spec.map φ)
inst : QuasiCompact (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).FinitePresentation

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)] at hf

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
φ : R ⟶ S
hf : LocallyOfFinitePresentation (Spec.map φ)
inst : QuasiCompact (Spec.map φ)
hf₁ : (CommRingCat.Hom.hom φ).FinitePresentation
⊢ QuasiCompact (Spec.map φ)

Tactic:
rw [HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)] at hf

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
φ : R ⟶ S
hf : (CommRingCat.Hom.hom φ).FinitePresentation
inst : QuasiCompact (Spec.map φ)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑(Spec.map φ) '' s)

Tactic:
(PrimeSpectrum.isConstructible_comap_image hf hs.isConstructible).isLocallyConstructible

Premises used: Topology.IsConstructible.isLocallyConstructible, Topology.IsLocallyConstructible.isConstructible, PrimeSpectrum.isConstructible_comap_image, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
R S : CommRingCat
s : Set ↥(Spec S)
hs : IsLocallyConstructible s
φ : R ⟶ S
hf : (CommRingCat.Hom.hom φ).FinitePresentation
inst : QuasiCompact (Spec.map φ)
⊢ IsLocallyConstructible (X := ↥(Spec R)) (⇑(Spec.map φ) '' s)

Tactic:
exact (PrimeSpectrum.isConstructible_comap_image hf hs.isConstructible).isLocallyConstructible

Premises used: Topology.IsConstructible.isLocallyConstructible, Topology.IsLocallyConstructible.isConstructible, PrimeSpectrum.isConstructible_comap_image
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : QuasiCompact f
inst_2 : CompactSpace.{u} ↥Y
inst_3 : QuasiSeparatedSpace.{u} ↥Y
s : Set ↥X
hs : IsConstructible s
⊢ IsConstructible (X := ↥Y) (⇑f '' s)

Tactic:
(f.isLocallyConstructible_image hs.isLocallyConstructible).isConstructible

Premises used: Topology.IsConstructible.isLocallyConstructible, Topology.IsLocallyConstructible.isConstructible, AlgebraicGeometry.Scheme.Hom.isLocallyConstructible_image
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
Goal:
X Y : Scheme
f : X ⟶ Y
s : Set ↥Y
hs : IsConstructible s
⊢ IsConstructible (X := ↥X) (⇑f ⁻¹' s)

Tactic:
hs.preimage f.continuous fun t ht ht' ↦ IsRetrocompact_iff_isSpectralMap_subtypeVal.mpr
    (quasiCompact_iff_isSpectralMap.mp
    (MorphismProperty.of_isPullback (P := @QuasiCompact)
    (isPullback_morphismRestrict f ⟨t, ht⟩)
    (quasiCompact_iff_isSpectralMap.mpr (IsRetrocompact_iff_isSpectralMap_subtypeVal.mp ht'))))

Premises used: Iff.mpr, CategoryTheory.MorphismProperty.of_isPullback, IsRetrocompact_iff_isSpectralMap_subtypeVal, TopologicalSpace.Opens.mk, AlgebraicGeometry.isPullback_morphismRestrict, Iff.mp, AlgebraicGeometry.Scheme.Hom.continuous, Topology.IsConstructible.preimage, AlgebraicGeometry.quasiCompact_iff_isSpectralMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    LocallyOfFiniteType f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
⊢ @LocallyOfFiniteType = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType

Tactic:
ext X Y f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
h :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f
h₁ h₂ :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType) ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType
⊢ LocallyOfFiniteType f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.FiniteType) f

Tactic:
rw [locallyOfFiniteType_iff, affineLocally_iff_forall_isAffineOpen]

Premises used: AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.locallyOfFiniteType_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ LocallyOfFiniteType f

Tactic:
HasRingHomProperty.of_isOpenImmersion
    RingHom.finiteType_holdsForLocalizationAway.containsIdentities

Premises used: RingHom.finiteType_holdsForLocalizationAway, RingHom.HoldsForLocalizationAway.containsIdentities, AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderComposition @LocallyOfFiniteType

Tactic:
HasRingHomProperty.stableUnderComposition RingHom.finiteType_stableUnderComposition

Premises used: AlgebraicGeometry.HasRingHomProperty.stableUnderComposition, RingHom.finiteType_stableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : LocallyOfFiniteType f
hg : LocallyOfFiniteType g
⊢ LocallyOfFiniteType (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ f g hf hg

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : LocallyOfFiniteType (f ≫ g)
⊢ LocallyOfFiniteType f

Tactic:
HasRingHomProperty.of_comp (fun _ _ ↦ RingHom.FiniteType.of_comp_finiteType) ‹_›

Premises used: AlgebraicGeometry.HasRingHomProperty.of_comp, RingHom.FiniteType.of_comp_finiteType
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderBaseChange @LocallyOfFiniteType

Tactic:
HasRingHomProperty.isStableUnderBaseChange RingHom.finiteType_isStableUnderBaseChange

Premises used: RingHom.finiteType_isStableUnderBaseChange, AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : LocallyOfFiniteType g
⊢ LocallyOfFiniteType (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.FiniteType
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : LocallyOfFiniteType f
⊢ LocallyOfFiniteType (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.FiniteType
Goal:
X Y : Scheme
f_1 f : X ⟶ Y
V : Y.Opens
inst : LocallyOfFiniteType f
⊢ LocallyOfFiniteType (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

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

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
x : ↥X
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).EssFiniteType

Tactic:
HasRingHomProperty.stalkMap_of_respectsIso RingHom.EssFiniteType.respectsIso
    (fun f hf _ _ ↦ RingHom.EssFiniteType.holdsForLocalization.localRingHom
      RingHom.EssFiniteType.stableUnderComposition
      RingHom.EssFiniteType.isStableUnderBaseChange.localizationPreserves _
      (RingHom.FiniteType.essFiniteType hf)) ‹_› x

Premises used: RingHom.EssFiniteType.isStableUnderBaseChange, RingHom.IsStableUnderBaseChange.localizationPreserves, RingHom.HoldsForLocalization.localRingHom, RingHom.EssFiniteType.respectsIso, RingHom.EssFiniteType.holdsForLocalization, AlgebraicGeometry.HasRingHomProperty.stalkMap_of_respectsIso, RingHom.FiniteType.essFiniteType, RingHom.EssFiniteType.stableUnderComposition, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
R : Type u_1
inst : CommRing R
inst_1 : IsJacobsonRing R
⊢ JacobsonSpace.{u_1} ↥(Spec (CommRingCat.of R))

Tactic:
inferInstanceAs (JacobsonSpace (PrimeSpectrum R))

Premises used: _private.0.AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfOfIsJacobsonRing._proof_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
R : CommRingCat
inst : IsJacobsonRing.{u_1} (↑R : Type u_1)
⊢ JacobsonSpace.{u_1} ↥(Spec R)

Tactic:
inferInstanceAs (JacobsonSpace (PrimeSpectrum R))

Premises used: _private.0.AlgebraicGeometry.instJacobsonSpaceCarrierCarrierCommRingCatSpecOfIsJacobsonRingCarrier._proof_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
        (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X)
    (hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
⊢ JacobsonSpace.{u} ↥X

Tactic:
wlog hY : ∃ S, Y = Spec S
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
inr :
  ∀ (i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀),
    JacobsonSpace.{u} ↥(Scheme.Hom.opensRange ((Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).f i))
⊢ JacobsonSpace.{u} ↥X

Tactic:
rw [(Scheme.OpenCover.isOpenCover_opensRange (Y.affineCover.pullback₁ f)).jacobsonSpace_iff]

Premises used: AlgebraicGeometry.Scheme.OpenCover.isOpenCover_opensRange, TopologicalSpace.IsOpenCover.jacobsonSpace_iff, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
⊢ LocallyOfFiniteType (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 inst : LocallyOfFiniteType (Y.affineCover.pullbackHom f i) :=
      MorphismProperty.pullback_snd _ _ inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst :
  LocallyOfFiniteType (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)
⊢ JacobsonSpace.{u} ↥Y

Tactic:
have inst : JacobsonSpace Y := ‹_›
-- Module: Mathlib.AlgebraicGeometry.Morphisms.FiniteType
Goal:
X Y : Scheme
f : X ⟶ Y
inst_1 : LocallyOfFiniteType f
inst_2 : JacobsonSpace.{u} ↥Y
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFiniteType f] [JacobsonSpace.{u} ↥Y]
    (hY : ∃ (S : CommRingCat.{u}), Y = Spec S), JacobsonSpace.{u} ↥X
hY : ¬∃ (S : CommRingCat.{u}), Y = Spec S
i : (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).I₀
inst_3 :
  LocallyOfFiniteType (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)
inst : JacobsonSpace.{u} ↥Y
⊢ JacobsonSpace.{u} ↥(Y.affineCover.X i)

Tactic:
have inst : JacobsonSpace (Y.affineCover.X i) :=
      .of_isOpenEmbedding (Y.affineCover.f i).isOpenEmbedding