awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : CommRingCat
inst : IsLocallyNoetherian.{u_1} (Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst_1 : LocallyOfFiniteType f
obtain : ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)], id (IsLocallyNoetherian.{u_1} (Spec S))
⊢ id (IsLocallyNoetherian.{u_1} (Spec S))

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

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : CommRingCat
inst : IsLocallyNoetherian.{u_1} (Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).FiniteType

Tactic:
have : φ.hom.FiniteType := HasRingHomProperty.Spec_iff.mp ‹_›
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : CommRingCat
inst : IsLocallyNoetherian.{u_1} (Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
this : (CommRingCat.Hom.hom φ).FiniteType
⊢ Algebra.FiniteType.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : CommRingCat
inst : IsLocallyNoetherian.{u_1} (Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
this : (CommRingCat.Hom.hom φ).FiniteType
algInst : Algebra (↑R : Type u_1) (↑S : Type u_1) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FiniteType.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
⊢ id (IsLocallyNoetherian.{u_1} (Spec S))

Tactic:
simp_all [Algebra.FiniteType.isNoetherianRing R]

Premises used: CommRingCat.carrier, Algebra.FiniteType.isNoetherianRing
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X_1 : Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsLocallyNoetherian Y
inst_1 : LocallyOfFiniteType f
⊢ IsLocallyNoetherian.{u_1} (Limits.pullback f g)

Tactic:
LocallyOfFiniteType.isLocallyNoetherian (Limits.pullback.snd _ _)

Premises used: AlgebraicGeometry.LocallyOfFiniteType.isLocallyNoetherian, CategoryTheory.Limits.pullback.snd
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X_1 : Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : IsLocallyNoetherian X
inst_1 : LocallyOfFiniteType g
⊢ IsLocallyNoetherian.{u_1} (Limits.pullback f g)

Tactic:
LocallyOfFiniteType.isLocallyNoetherian (Limits.pullback.fst _ _)

Premises used: AlgebraicGeometry.LocallyOfFiniteType.isLocallyNoetherian, CategoryTheory.Limits.pullback.fst
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X_1 : Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyNoetherian Y
inst_1 : LocallyOfFiniteType f
⊢ LocallyOfFinitePresentation f

Tactic:
⟨fun {U hU V hV} hUV ↦ ?_⟩

Premises used: AlgebraicGeometry.LocallyOfFinitePresentation.mk
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X_1 : Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyNoetherian Y
inst_1 : LocallyOfFiniteType f
refine :
  ∀ {U : Y.Opens} {hU : IsAffineOpen U} {V : X.Opens} {hV : IsAffineOpen V} (hUV : V ≤ f ⁻¹ᵁ U),
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FinitePresentation
⊢ LocallyOfFinitePresentation f

Tactic:
refine ⟨fun {U hU V hV} hUV ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X_1 : Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyNoetherian Y
inst_1 : LocallyOfFiniteType f
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hUV : V ≤ f ⁻¹ᵁ U
this : Algebra (↑Γ(Y, U) : Type u_1) (↑Γ(X, V) : Type u_1) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
⊢ IsNoetherianRing.{u_1} (↑Γ(Y, U) : Type u_1)

Tactic:
have : IsNoetherianRing Γ(Y, U) := IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X_1 : Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyNoetherian Y
inst_1 : LocallyOfFiniteType f
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hUV : V ≤ f ⁻¹ᵁ U
this_1 : Algebra (↑Γ(Y, U) : Type u_1) (↑Γ(X, V) : Type u_1) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
this : IsNoetherianRing.{u_1} (↑Γ(Y, U) : Type u_1)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FinitePresentation

Tactic:
Algebra.FinitePresentation.of_finiteType.mp (f.finiteType_appLE hU hV hUV)

Premises used: RingHom.FinitePresentation, AlgebraicGeometry.Scheme.Hom.finiteType_appLE, Algebra.FinitePresentation.of_finiteType, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X_1 : Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyNoetherian Y
inst_1 : LocallyOfFiniteType f
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hUV : V ≤ f ⁻¹ᵁ U
this_1 : Algebra (↑Γ(Y, U) : Type u_1) (↑Γ(X, V) : Type u_1) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).toAlgebra
this : IsNoetherianRing.{u_1} (↑Γ(Y, U) : Type u_1)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FinitePresentation

Tactic:
exact Algebra.FinitePresentation.of_finiteType.mp (f.finiteType_appLE hU hV hUV)

Premises used: AlgebraicGeometry.Scheme.Hom.finiteType_appLE, Algebra.FinitePresentation.of_finiteType, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyNoetherian Y
⊢ LocallyOfFinitePresentation f ↔ LocallyOfFiniteType f

Tactic:
⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
mp : IsNoetherian X → ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
mpr : (∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)) → IsNoetherian X
⊢ IsNoetherian X ↔ ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : IsNoetherian X
i : ι
mp : IsLocallyNoetherian X
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)

Tactic:
apply (isLocallyNoetherian_iff_of_iSup_eq_top hS).mp

Premises used: AlgebraicGeometry.isLocallyNoetherian_iff_of_iSup_eq_top, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : IsNoetherian X
i : ι
⊢ IsLocallyNoetherian X

Tactic:
h.toIsLocallyNoetherian

Premises used: AlgebraicGeometry.IsNoetherian.toIsLocallyNoetherian
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : IsNoetherian X
i : ι
⊢ IsLocallyNoetherian X

Tactic:
exact h.toIsLocallyNoetherian

Premises used: AlgebraicGeometry.IsNoetherian.toIsLocallyNoetherian
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
⊢ IsNoetherian X

Tactic:
IsNoetherian.mk

Premises used: AlgebraicGeometry.IsNoetherian.mk
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
mpr : IsLocallyNoetherian X
mpr₁ : CompactSpace.{u_2} ↥X
⊢ IsNoetherian X

Tactic:
convert! IsNoetherian.mk

Premises used: AlgebraicGeometry.IsNoetherian.mk
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
⊢ IsLocallyNoetherian X

Tactic:
isLocallyNoetherian_of_affine_cover hS h

Premises used: AlgebraicGeometry.isLocallyNoetherian_of_affine_cover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
⊢ IsLocallyNoetherian X

Tactic:
exact isLocallyNoetherian_of_affine_cover hS h

Premises used: AlgebraicGeometry.isLocallyNoetherian_of_affine_cover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
mpr : IsCompact.{u_2} (X := ↥X) Set.univ
⊢ CompactSpace.{u_2} ↥X

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
mpr : IsCompact (↑{ carrier := ⋃ (i : ι), Opens.carrier (S i).1, is_open' := ⋯ : Opens ↥X } : Set ↥X)
⊢ IsCompact.{u_2} (X := ↥X) Set.univ

Tactic:
rw [← Opens.coe_top, ← hS, Opens.iSup_mk]

Premises used: TopologicalSpace.Opens.iSup_mk, TopologicalSpace.Opens.coe_top
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
mpr : ∀ (i : ι), IsCompact.{u_2} (X := ↥X) (Opens.carrier (S i).1)
⊢ IsCompact (↑{ carrier := ⋃ (i : ι), Opens.carrier (S i).1, is_open' := ⋯ : Opens ↥X } : Set ↥X)

Tactic:
apply isCompact_iUnion

Premises used: isCompact_iUnion
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
i : ι
mpr : IsCompact.{u_2} (X := (↑(Opens.carrier (S i).1) : Type u_2)) Set.univ
⊢ IsCompact.{u_2} (X := ↥X) (Opens.carrier (S i).1)

Tactic:
apply isCompact_iff_isCompact_univ.mpr

Premises used: Iff.mpr, isCompact_iff_isCompact_univ
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
i : ι
⊢ IsCompact.{u_2} (X := (↑(Opens.carrier (S i).1) : Type u_2)) Set.univ

Tactic:
CompactSpace.isCompact_univ

Premises used: CompactSpace.isCompact_univ
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
i : ι
mpr : CompactSpace.{u_2} (↑(Opens.carrier (S i).1) : Type u_2)
⊢ IsCompact.{u_2} (X := (↑(Opens.carrier (S i).1) : Type u_2)) Set.univ

Tactic:
convert! CompactSpace.isCompact_univ

Premises used: CompactSpace.isCompact_univ
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
i : ι
⊢ NoetherianSpace.{u_2} ↥(↑(↑(S i) : X.Opens) : Scheme)

Tactic:
apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2

Premises used: AlgebraicGeometry.noetherianSpace_of_isAffineOpen, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
i : ι
⊢ NoetherianSpace.{u_2} ↥(↑(↑(S i) : X.Opens) : Scheme)

Tactic:
have : NoetherianSpace (S i) := by
        apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
inst : Finite ι
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
h : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
i : ι
this : NoetherianSpace.{u_2} ↥(↑(↑(S i) : X.Opens) : Scheme)
⊢ CompactSpace.{u_2} (↑(Opens.carrier (S i).1) : Type u_2)

Tactic:
apply NoetherianSpace.compactSpace (S i)

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Subtype.val, AlgebraicGeometry.Scheme.Opens.toScheme, TopologicalSpace.NoetherianSpace.compactSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
mp : IsNoetherian X → ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
mpr : (∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)) → IsNoetherian X
⊢ IsNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
h : IsNoetherian X
i : 𝒰.I₀
mp : IsLocallyNoetherian X
⊢ IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)

Tactic:
apply (isLocallyNoetherian_iff_of_affine_openCover _).mp

Premises used: AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
h : IsNoetherian X
i : 𝒰.I₀
⊢ IsLocallyNoetherian X

Tactic:
h.toIsLocallyNoetherian

Premises used: AlgebraicGeometry.IsNoetherian.toIsLocallyNoetherian
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
h : IsNoetherian X
i : 𝒰.I₀
⊢ IsLocallyNoetherian X

Tactic:
exact h.toIsLocallyNoetherian

Premises used: AlgebraicGeometry.IsNoetherian.toIsLocallyNoetherian
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
⊢ IsNoetherian X

Tactic:
IsNoetherian.mk

Premises used: AlgebraicGeometry.IsNoetherian.mk
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
mpr : IsLocallyNoetherian X
mpr₁ : CompactSpace.{u} ↥X
⊢ IsNoetherian X

Tactic:
convert! IsNoetherian.mk

Premises used: AlgebraicGeometry.IsNoetherian.mk
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
⊢ IsLocallyNoetherian X

Tactic:
(isLocallyNoetherian_iff_of_affine_openCover _).mpr hNoeth

Premises used: Iff.mpr, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
⊢ IsLocallyNoetherian X

Tactic:
exact (isLocallyNoetherian_iff_of_affine_openCover _).mpr hNoeth

Premises used: Iff.mpr, AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
⊢ CompactSpace.{u} ↥X

Tactic:
Scheme.OpenCover.compactSpace 𝒰

Premises used: AlgebraicGeometry.Scheme.OpenCover.compactSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
⊢ CompactSpace.{u} ↥X

Tactic:
exact Scheme.OpenCover.compactSpace 𝒰

Premises used: AlgebraicGeometry.Scheme.OpenCover.compactSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
apply : NoetherianSpace.{u_1} (↑Set.univ : Type u_1)
⊢ NoetherianSpace.{u_1} ↥X

Tactic:
apply TopologicalSpace.noetherian_univ_iff.mp

Premises used: TopologicalSpace.noetherian_univ_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
rw : NoetherianSpace.{u_1} (↑(⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)
⊢ NoetherianSpace.{u_1} (↑Set.univ : Type u_1)

Tactic:
rw [← 𝒰.iUnion_range]

Premises used: AlgebraicGeometry.Scheme.Cover.iUnion_range
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
this : ∀ (i : 𝒰.I₀), NoetherianSpace.{u_1} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)
⊢ NoetherianSpace.{u_1} (↑(⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)

Tactic:
apply NoetherianSpace.iUnion

Premises used: TopologicalSpace.NoetherianSpace.iUnion
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
suffices : ∀ (i : 𝒰.I₀), NoetherianSpace.{u_1} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)
⊢ NoetherianSpace.{u_1} (↑(⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)

Tactic:
suffices ∀ i : 𝒰.I₀, NoetherianSpace (Set.range <| (𝒰.f i)) by
    apply NoetherianSpace.iUnion
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
rw : IsAffine.{u_1} (X.affineCover.X (Scheme.Cover.idx X.affineCover (↑i : ↥X)))
⊢ IsAffine.{u_1} (𝒰.X i)

Tactic:
rw [X.affineCover.finiteSubcover_X]

Premises used: AlgebraicGeometry.Scheme.OpenCover.finiteSubcover_X, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
⊢ IsAffine.{u_1} (X.affineCover.X (Scheme.Cover.idx X.affineCover (↑i : ↥X)))

Tactic:
apply Scheme.isAffine_affineCover

Premises used: AlgebraicGeometry.Scheme.isAffine_affineCover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
⊢ IsAffine.{u_1} (𝒰.X i)

Tactic:
have : IsAffine (𝒰.X i) := by
    rw [X.affineCover.finiteSubcover_X]
    apply Scheme.isAffine_affineCover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
this : IsAffine.{u_1} (𝒰.X i)
U : (↑X.affineOpens : Type u_1) :=
  Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
⊢ NoetherianSpace.{u_1} ↥(↑(↑U : X.Opens) : Scheme)

Tactic:
noetherianSpace_of_isAffineOpen U.1 U.2

Premises used: AlgebraicGeometry.noetherianSpace_of_isAffineOpen, Subtype.val, Subtype.property
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
this : IsAffine.{u_1} (𝒰.X i)
U : (↑X.affineOpens : Type u_1) :=
  Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
convert! : IsNoetherianRing.{u_1} (↑Γ(X, (↑U : X.Opens)) : Type u_1)
⊢ NoetherianSpace.{u_1} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)

Tactic:
convert! noetherianSpace_of_isAffineOpen U.1 U.2
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
this : IsAffine.{u_1} (𝒰.X i)
U : (↑X.affineOpens : Type u_1) :=
  Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
⊢ IsNoetherianRing.{u_1} (↑Γ(X, (↑U : X.Opens)) : Type u_1)

Tactic:
apply IsLocallyNoetherian.component_noetherian

Premises used: AlgebraicGeometry.IsLocallyNoetherian.component_noetherian
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X_1 : Scheme
X Y : Scheme
inst : NoetherianSpace.{u_1} ↥X
f : X ⟶ Y
⊢ QuasiCompact f

Tactic:
⟨fun _ _ _ => NoetherianSpace.isCompact _⟩

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Set.preimage, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.QuasiCompact.mk, DFunLike.coe, TopologicalSpace.NoetherianSpace.isCompact
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
this : IsNoetherianRing.{u_1} (↑(CommRingCat.of R) : Type u_1)
⊢ IsNoetherian.{u_1} (Spec (CommRingCat.of R))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
suffices : IsNoetherianRing.{u_1} (↑(CommRingCat.of R) : Type u_1)
⊢ IsNoetherian.{u_1} (Spec (CommRingCat.of R))

Tactic:
suffices IsNoetherianRing (CommRingCat.of R) by infer_instance
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ IsNoetherianRing.{u_1} (↑(CommRingCat.of R) : Type u_1)

Tactic:
assumption
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
x : ↥X
⊢ Membership.mem (γ := X.Opens) ⊤ x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
x : ↥X
obtain :
  ∀ (U : X.Opens) (hU : IsAffineOpen U) (hU2 : x ∈ U) (hU3 : U.carrier ⊆ (↑⊤ : Set ↥X)),
    IsNoetherianRing.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
⊢ IsNoetherianRing.{u_1} (↑(X.presheaf.stalk x) : Type u_1)

Tactic:
obtain ⟨U, hU, hU2, hU3⟩ := exists_isAffineOpen_mem_and_subset (U := ⊤) (x := x) (by simp)

Premises used: AlgebraicGeometry.exists_isAffineOpen_mem_and_subset
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
x : ↥X
U : X.Opens
hU : IsAffineOpen U
hU2 : x ∈ U
hU3 : U.carrier ⊆ (↑⊤ : Set ↥X)
⊢ IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hU2) : ↥X)) : Type u_1)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hU2)).asIdeal

Tactic:
have := AlgebraicGeometry.IsAffineOpen.isLocalization_stalk hU ⟨x, hU2⟩
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
x : ↥X
U : X.Opens
hU : IsAffineOpen U
hU2 : x ∈ U
hU3 : U.carrier ⊆ (↑⊤ : Set ↥X)
this :
  IsLocalization.AtPrime (↑(X.presheaf.stalk (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hU2) : ↥X)) : Type u_1)
    (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hU2)).asIdeal
⊢ IsNoetherianRing.{u_1} (↑(X.presheaf.stalk x) : Type u_1)

Tactic:
@IsLocalization.isNoetherianRing _ _ (hU.primeIdealOf ⟨x, hU2⟩).asIdeal.primeCompl
        (X.presheaf.stalk x) _ (X.presheaf.algebra_section_stalk ⟨x, hU2⟩)
        this (IsLocallyNoetherian.component_noetherian ⟨U, hU⟩)

Premises used: CommRingCat.carrier, IsLocalization.isNoetherianRing, TopCat.Presheaf.stalk, Subtype.mk, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian, AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Ideal.primeCompl, PrimeSpectrum.asIdeal, AlgebraicGeometry.Scheme.toLocallyRingedSpace