awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
hCNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
fS : (i : 𝒰.I₀) → (↑X.affineOpens : Type u) :=
  fun (i : 𝒰.I₀) ↦ Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) (Scheme.Hom.opensRange (𝒰.f i)) ⋯
i : 𝒰.I₀
⊢ Γ(𝒰.X i, ⊤) ≅ Γ(X, (↑(fS i) : X.Opens))

Tactic:
exact IsOpenImmersion.ΓIsoTop (𝒰.f i)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsOpenImmersion.ΓIsoTop, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
U : X.Opens
inst : IsLocallyNoetherian X
⊢ IsLocallyNoetherian.{u_1} (↑U : Scheme)

Tactic:
isLocallyNoetherian_of_isOpenImmersion U.ι

Premises used: AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
U : Scheme.OpenCover.{u_1, u_2} X
i : U.I₀
inst : IsLocallyNoetherian X
⊢ IsLocallyNoetherian.{u_2} (U.X i)

Tactic:
isLocallyNoetherian_of_isOpenImmersion (U.f i)

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.isLocallyNoetherian_of_isOpenImmersion, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)

Tactic:
⟨fun _ ↦ inferInstance, ?_⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
refine : (∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)) → IsLocallyNoetherian X
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)

Tactic:
refine ⟨fun _ ↦ inferInstance, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
rw :
  (∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)) →
    ∀ (i : 𝒰.affineRefinement.openCover.I₀), IsNoetherianRing.{u_2} (↑Γ(𝒰.affineRefinement.openCover.X i, ⊤) : Type u_2)
⊢ (∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)) → IsLocallyNoetherian X

Tactic:
rw [isLocallyNoetherian_iff_of_affine_openCover (𝒰 := 𝒰.affineRefinement.openCover)]

Premises used: AlgebraicGeometry.isLocallyNoetherian_iff_of_affine_openCover, AlgebraicGeometry.Scheme.AffineOpenCover.openCover, AlgebraicGeometry.Scheme.OpenCover.affineRefinement
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
h : ∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)
i : 𝒰.affineRefinement.openCover.I₀
⊢ IsNoetherianRing.{u_2} (↑Γ(𝒰.affineRefinement.openCover.X i, ⊤) : Type u_2)

Tactic:
@isNoetherianRing_of_ringEquiv _ _ _ _
      (IsOpenImmersion.ΓIsoTop (PreZeroHypercover.f _ i.2)).symm.commRingCatIsoToRingEquiv
      (IsLocallyNoetherian.component_noetherian ⟨_, isAffineOpen_opensRange _⟩)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsOpenImmersion.ΓIsoTop, CategoryTheory.Iso.symm, Sigma.snd, isNoetherianRing_of_ringEquiv
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
h : ∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)
i : 𝒰.affineRefinement.openCover.I₀
⊢ IsNoetherianRing.{u_2} (↑Γ(𝒰.affineRefinement.openCover.X i, ⊤) : Type u_2)

Tactic:
exact @isNoetherianRing_of_ringEquiv _ _ _ _
      (IsOpenImmersion.ΓIsoTop (PreZeroHypercover.f _ i.2)).symm.commRingCatIsoToRingEquiv
      (IsLocallyNoetherian.component_noetherian ⟨_, isAffineOpen_opensRange _⟩)

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv, CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsOpenImmersion.ΓIsoTop, CategoryTheory.Iso.symm, Sigma.snd, isNoetherianRing_of_ringEquiv
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
R : CommRingCat
inst : IsNoetherianRing.{u_1} (↑R : Type u_1)
⊢ NoetherianSpace.{u_1} (PrimeSpectrum (↑R : Type u_1))

Tactic:
PrimeSpectrum.instNoetherianSpace (R := R)

Premises used: CommRingCat.carrier, PrimeSpectrum.instNoetherianSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
R : CommRingCat
inst : IsNoetherianRing.{u_1} (↑R : Type u_1)
⊢ NoetherianSpace.{u_1} ↥(Spec R)

Tactic:
convert! PrimeSpectrum.instNoetherianSpace (R := R)

Premises used: CommRingCat.carrier, PrimeSpectrum.instNoetherianSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsAffine X
inst_1 : IsNoetherianRing.{u_1} (↑Γ(X, ⊤) : Type u_1)
⊢ NoetherianSpace.{u_1} ↥X

Tactic:
(noetherianSpace_iff_of_homeomorph X.isoSpec.inv.homeomorph).mp inferInstance

Premises used: AlgebraicGeometry.Scheme.isoSpec, TopologicalSpace.noetherianSpace_iff_of_homeomorph, inferInstance, AlgebraicGeometry.Scheme.Hom.homeomorph, Iff.mp, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst : IsNoetherianRing.{u_1} (↑Γ(X, U) : Type u_1)
⊢ IsNoetherianRing.{u_1} (↑Γ((↑U : Scheme), ⊤) : Type u_1)

Tactic:
have : IsNoetherianRing Γ(U, ⊤) := isNoetherianRing_of_ringEquiv _
    (Scheme.restrictFunctorΓ.app (op U)).symm.commRingCatIsoToRingEquiv
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst : IsNoetherianRing.{u_1} (↑Γ(X, U) : Type u_1)
this : IsNoetherianRing.{u_1} (↑Γ((↑U : Scheme), ⊤) : Type u_1)
⊢ NoetherianSpace.{u_1} ↥(↑U : Scheme)

Tactic:
@noetherianSpace_of_isAffine _ hU _

Premises used: AlgebraicGeometry.noetherianSpace_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst : IsNoetherianRing.{u_1} (↑Γ(X, U) : Type u_1)
this : IsNoetherianRing.{u_1} (↑Γ((↑U : Scheme), ⊤) : Type u_1)
⊢ NoetherianSpace.{u_1} ↥(↑U : Scheme)

Tactic:
exact @noetherianSpace_of_isAffine _ hU _

Premises used: AlgebraicGeometry.noetherianSpace_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
R : CommRingCat
inst : IsNoetherianRing.{u_1} (↑R : Type u_1)
⊢ Eq.{u_1 + 1} (α := (Spec R).Opens)
    (⨆ (i : Unit),
      (↑((fun (x : Unit) ↦
              (Subtype.mk (p := fun (x : (Spec R).Opens) ↦
                  Membership.mem (γ := Set (Spec R).Opens) (Spec R).affineOpens x) ⊤ ⋯ :
                { x : (Spec R).Opens // Membership.mem (γ := Set (Spec R).Opens) (Spec R).affineOpens x }))
            i) :
        (Spec R).Opens))
    ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
apply : ∀ (U : X.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥Z)
⊢ QuasiCompact f

Tactic:
apply quasiCompact_iff_forall_isAffineOpen.mpr

Premises used: Iff.mpr, AlgebraicGeometry.quasiCompact_iff_forall_isAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
rw : IsCompact (X := ↥Z) (⇑f ⁻¹' ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f))
⊢ IsCompact (↑(f ⁻¹ᵁ U) : Set ↥Z)

Tactic:
rw [Opens.map_coe, ← Set.preimage_inter_range]

Premises used: TopologicalSpace.Opens.map_coe, Set.preimage_inter_range
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
hK : IsCompact ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f)
Kf : (↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f ⊆ Set.range (ι := ↥Z) ⇑f
⊢ IsCompact (X := ↥Z) (⇑f ⁻¹' ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f))

Tactic:
apply f.isOpenEmbedding.isInducing.isCompact_preimage'

Premises used: AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, Topology.IsOpenEmbedding.isInducing, Topology.IsInducing.isCompact_preimage'
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
hK : NoetherianSpace.{u_1} (↑(↑U : Set ↥X) : Type u_1)
hK₁ : (↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f ⊆ (↑U : Set ↥X)
apply : Set ↥X
⊢ IsCompact ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f)

Tactic:
apply (noetherianSpace_set_iff _).mp

Premises used: TopologicalSpace.noetherianSpace_set_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ NoetherianSpace.{u_1} ↥(↑U : Scheme)

Tactic:
noetherianSpace_of_isAffineOpen U hU

Premises used: AlgebraicGeometry.noetherianSpace_of_isAffineOpen
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
hK : IsNoetherianRing.{u_1} (↑Γ(X, U) : Type u_1)
⊢ NoetherianSpace.{u_1} (↑(↑U : Set ↥X) : Type u_1)

Tactic:
convert! noetherianSpace_of_isAffineOpen U hU
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsNoetherianRing.{u_1} (↑Γ(X, U) : Type u_1)

Tactic:
apply IsLocallyNoetherian.component_noetherian ⟨U, hU⟩

Premises used: Subtype.mk, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ (↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f ⊆ (↑U : Set ↥X)

Tactic:
Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ (↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f ⊆ (↑U : Set ↥X)

Tactic:
exact Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ (↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f ⊆ Set.range (ι := ↥Z) ⇑f

Tactic:
Set.inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ (↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f ⊆ Set.range (ι := ↥Z) ⇑f

Tactic:
exact Set.inter_subset_right

Premises used: Set.inter_subset_right
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
apply : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
⊢ QuasiSeparatedSpace.{u_1} ↥X

Tactic:
apply quasiSeparatedSpace_iff_forall_affineOpens.mpr

Premises used: Iff.mpr, AlgebraicGeometry.quasiSeparatedSpace_iff_forall_affineOpens
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
⊢ Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
have hInd := U.2.fromSpec.isOpenEmbedding.isInducing
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
apply :
  IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
    (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
apply₁ :
  (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ⊆
    Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))

Tactic:
apply (hInd.isCompact_preimage_iff ?_).mp

Premises used: Iff.mp, Topology.IsInducing.isCompact_preimage_iff
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
rw :
  IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
    (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹'
      ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))))
⊢ IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
    (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))

Tactic:
rw [← Set.preimage_inter_range, IsAffineOpen.range_fromSpec, Set.inter_comm]

Premises used: Set.preimage_inter_range, Set.inter_comm, AlgebraicGeometry.IsAffineOpen.range_fromSpec
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
hK : IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
Kf :
  (↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) ⊆
    Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯)
⊢ IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
    (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹'
      ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))))

Tactic:
apply hInd.isCompact_preimage'

Premises used: Topology.IsInducing.isCompact_preimage'
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
hK : NoetherianSpace.{u_1} (↑(↑(↑U : X.Opens) : Set ↥X) : Type u_1)
hK₁ :
  (↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) ⊆ (↑(↑U : X.Opens) : Set ↥X)
apply : Set ↥X
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))

Tactic:
apply (noetherianSpace_set_iff _).mp

Premises used: TopologicalSpace.noetherianSpace_set_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
⊢ 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 : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
hK : IsNoetherianRing.{u_1} (↑Γ(X, (↑U : X.Opens)) : Type u_1)
⊢ NoetherianSpace.{u_1} (↑(↑(↑U : X.Opens) : Set ↥X) : Type u_1)

Tactic:
convert! noetherianSpace_of_isAffineOpen U.1 U.2
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
⊢ 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 : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
⊢ (↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) ⊆ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
⊢ (↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) ⊆ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
exact Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
Kf : (↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) ⊆ (↑(↑U : X.Opens) : Set ↥X)
⊢ (↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) ⊆
    Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
rw [IsAffineOpen.range_fromSpec]

Premises used: AlgebraicGeometry.IsAffineOpen.range_fromSpec
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
rw : (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ⊆ (↑(↑U : X.Opens) : Set ↥X)
⊢ (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ⊆
    Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯)

Tactic:
rw [IsAffineOpen.range_fromSpec]

Premises used: AlgebraicGeometry.IsAffineOpen.range_fromSpec
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
⊢ (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ⊆ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec ⋯)
⊢ (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ⊆ (↑(↑U : X.Opens) : Set ↥X)

Tactic:
exact Set.inter_subset_left

Premises used: Set.inter_subset_left
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
        (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R), id (IsLocallyNoetherian X))
    (hY : ¬∃ (R : CommRingCat.{u_1}), Y = Spec R), id (IsLocallyNoetherian X)
wlog :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
    (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R), id (IsLocallyNoetherian X)
⊢ id (IsLocallyNoetherian X)

Tactic:
wlog hY : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
this :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
    (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R), id (IsLocallyNoetherian X)
hY : ¬∃ (R : CommRingCat.{u_1}), Y = Spec R
⊢ id (IsLocallyNoetherian X)

Tactic:
(isLocallyNoetherian_iff_openCover (Y.affineCover.pullback₁ f)).mpr fun i ↦
      this (Limits.pullback.snd f (Y.affineCover.f i)) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
this :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
    (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R), id (IsLocallyNoetherian X)
hY : ¬∃ (R : CommRingCat.{u_1}), Y = Spec R
⊢ id (IsLocallyNoetherian X)

Tactic:
exact (isLocallyNoetherian_iff_openCover (Y.affineCover.pullback₁ f)).mpr fun i ↦
      this (Limits.pullback.snd f (Y.affineCover.f i)) ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, CategoryTheory.Limits.pullback.snd, Exists.intro, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, CategoryTheory.Precoverage.ZeroHypercover.pullback₁, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
        (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R) (hX : ∃ (S : CommRingCat.{u_1}), X = Spec S),
        id (IsLocallyNoetherian X))
    (hX : ¬∃ (S : CommRingCat.{u_1}), X = Spec S), id (IsLocallyNoetherian X)
wlog :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
    (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R) (hX : ∃ (S : CommRingCat.{u_1}), X = Spec S),
    id (IsLocallyNoetherian X)
⊢ id (IsLocallyNoetherian X)

Tactic:
wlog hX : ∃ S, X = Spec S
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R
this :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
    (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R) (hX : ∃ (S : CommRingCat.{u_1}), X = Spec S),
    id (IsLocallyNoetherian X)
hX : ¬∃ (S : CommRingCat.{u_1}), X = Spec S
⊢ id (IsLocallyNoetherian X)

Tactic:
(isLocallyNoetherian_iff_openCover X.affineCover).mpr
      fun i ↦ this (X.affineCover.f i ≫ f) hY ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R
this :
  ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
    (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R) (hX : ∃ (S : CommRingCat.{u_1}), X = Spec S),
    id (IsLocallyNoetherian X)
hX : ¬∃ (S : CommRingCat.{u_1}), X = Spec S
⊢ id (IsLocallyNoetherian X)

Tactic:
exact (isLocallyNoetherian_iff_openCover X.affineCover).mpr
      fun i ↦ this (X.affineCover.f i ≫ f) hY ⟨_, rfl⟩

Premises used: Iff.mpr, CategoryTheory.PreZeroHypercover.f, Exists.intro, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.Scheme.affineCover._proof_7, Classical.choose, AlgebraicGeometry.isLocallyNoetherian_iff_openCover, AlgebraicGeometry.Scheme.affineCover, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, rfl
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R
hX : ∃ (S : CommRingCat.{u_1}), X = Spec S
obtain :
  ∀ (R : CommRingCat.{u_1}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [IsLocallyNoetherian.{u_1} (Spec R)],
    id (IsLocallyNoetherian X)
⊢ id (IsLocallyNoetherian X)

Tactic:
obtain ⟨R, rfl⟩ := hY

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
hX : ∃ (S : CommRingCat.{u_1}), X = Spec S
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian.{u_1} (Spec R)
obtain :
  ∀ (S : CommRingCat.{u_1}) (f : Spec S ⟶ Spec R) [LocallyOfFiniteType f], id (IsLocallyNoetherian.{u_1} (Spec S))
⊢ id (IsLocallyNoetherian X)

Tactic:
obtain ⟨S, rfl⟩ := hX

Premises used: rfl