awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)))
⊢ IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
    (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹'
      ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))))
have 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 sorry)
Tactic: apply hInd.isCompact_preimage'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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 ⋯)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
have hK : NoetherianSpace.{u_1} (↑(↑(↑U : X.Opens) : Set ↥X) : Type u_1)
Tactic: apply (noetherianSpace_set_iff _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
have hK₁ : (↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) ⊆ (↑(↑U : X.Opens) : Set ↥X)
Tactic: apply (noetherianSpace_set_iff _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
have apply : Set ↥X
Tactic: apply (noetherianSpace_set_iff _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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) : Set ↥X) : Type u_1)
have hK : IsNoetherianRing.{u_1} (↑Γ(X, (↑U : X.Opens)) : Type u_1)
Tactic: convert! noetherianSpace_of_isAffineOpen U.1 U.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)) ⊆
    Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯)
have Kf : (↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)) ⊆ (↑(↑U : X.Opens) : Set ↥X)
Tactic: rw [IsAffineOpen.range_fromSpec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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) ⊆
    Set.range (ι := ↥(Spec Γ(X, (↑U : X.Opens)))) ⇑(IsAffineOpen.fromSpec ⋯)
have rw : (↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X) ⊆ (↑(↑U : X.Opens) : Set ↥X)
Tactic: rw [IsAffineOpen.range_fromSpec]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
⊢ id (IsLocallyNoetherian X)
have 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)
Tactic: wlog hY : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ id (IsLocallyNoetherian X)
have wlog : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y) [LocallyOfFiniteType f] [IsLocallyNoetherian Y]
  (hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R), id (IsLocallyNoetherian X)
Tactic: wlog hY : ∃ R, Y = Spec R
Cleared hypotheses: X, Y, f, inst, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFiniteType f
inst_1 : IsLocallyNoetherian Y
hY : ∃ (R : CommRingCat.{u_1}), Y = Spec R
⊢ id (IsLocallyNoetherian X)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ id (IsLocallyNoetherian X)
have 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)
Tactic: wlog hX : ∃ S, X = Spec S
Cleared hypotheses: X, Y, f, inst, inst_1, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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
⊢ id (IsLocallyNoetherian X)
have obtain : ∀ (R : CommRingCat.{u_1}) (f : X ⟶ Spec R) [LocallyOfFiniteType f] [IsLocallyNoetherian.{u_1} (Spec R)],
  id (IsLocallyNoetherian X)
Tactic: obtain ⟨R, rfl⟩ := hY
Cleared hypotheses: Y, f, inst, inst_1, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ id (IsLocallyNoetherian X)
have obtain : ∀ (S : CommRingCat.{u_1}) (f : Spec S ⟶ Spec R) [LocallyOfFiniteType f], id (IsLocallyNoetherian.{u_1} (Spec S))
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, hX, f, inst
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
R : CommRingCat
inst : IsLocallyNoetherian.{u_1} (Spec R)
S : CommRingCat
f : Spec S ⟶ Spec R
inst_1 : LocallyOfFiniteType f
⊢ id (IsLocallyNoetherian.{u_1} (Spec S))
have obtain : ∀ (φ : R ⟶ S) [LocallyOfFiniteType (Spec.map φ)], id (IsLocallyNoetherian.{u_1} (Spec S))
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f, inst_1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
R : CommRingCat
inst : IsLocallyNoetherian.{u_1} (Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
⊢ id (IsLocallyNoetherian.{u_1} (Spec S))
have this : (CommRingCat.Hom.hom φ).FiniteType
Tactic: have : φ.hom.FiniteType := HasRingHomProperty.Spec_iff.mp ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
R : CommRingCat
inst : IsLocallyNoetherian.{u_1} (Spec R)
S : CommRingCat
φ : R ⟶ S
inst_1 : LocallyOfFiniteType (Spec.map φ)
this : (CommRingCat.Hom.hom φ).FiniteType
⊢ id (IsLocallyNoetherian.{u_1} (Spec S))
have algebraizeInst : Algebra.FiniteType.{u_1, u_1} (↑R : Type u_1) (↑S : Type u_1)
Tactic: algebraize [φ.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X_1 : Scheme
X Y : Scheme
f : X ⟶ Y
inst : IsLocallyNoetherian Y
inst_1 : LocallyOfFiniteType f
⊢ LocallyOfFinitePresentation f
have 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
Tactic: refine ⟨fun {U hU V hV} hUV ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
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
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hUV)).FinitePresentation
have this₁ : IsNoetherianRing.{u_1} (↑Γ(Y, U) : Type u_1)
Tactic: have : IsNoetherianRing Γ(Y, U) := IsLocallyNoetherian.component_noetherian ⟨U, hU⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)) ⊤
⊢ IsNoetherian X ↔ ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
have mp : IsNoetherian X → ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsNoetherian X ↔ ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
have mpr : (∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)) → IsNoetherian X
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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 : ι
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
have mp : IsLocallyNoetherian X
Tactic: apply (isLocallyNoetherian_iff_of_iSup_eq_top hS).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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
have mpr : IsLocallyNoetherian X
Tactic: convert! IsNoetherian.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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
⊢ IsNoetherian X
have mpr₁ : CompactSpace.{u_2} ↥X
Tactic: convert! IsNoetherian.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ CompactSpace.{u_2} ↥X
have mpr : IsCompact.{u_2} (X := ↥X) Set.univ
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsCompact.{u_2} (X := ↥X) Set.univ
have mpr : IsCompact (↑{ carrier := ⋃ (i : ι), Opens.carrier (S i).1, is_open' := sorry : Opens ↥X } : Set ↥X)
Tactic: rw [← Opens.coe_top, ← hS, Opens.iSup_mk]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsCompact (↑{ carrier := ⋃ (i : ι), Opens.carrier (S i).1, is_open' := ⋯ : Opens ↥X } : Set ↥X)
have mpr : ∀ (i : ι), IsCompact.{u_2} (X := ↥X) (Opens.carrier (S i).1)
Tactic: apply isCompact_iUnion
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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 := ↥X) (Opens.carrier (S i).1)
have mpr : IsCompact.{u_2} (X := (↑(Opens.carrier (S i).1) : Type u_2)) Set.univ
Tactic: apply isCompact_iff_isCompact_univ.mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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
have mpr : CompactSpace.{u_2} (↑(Opens.carrier (S i).1) : Type u_2)
Tactic: convert! CompactSpace.isCompact_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
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 : ι
⊢ CompactSpace.{u_2} (↑(Opens.carrier (S i).1) : Type u_2)
have this : NoetherianSpace.{u_2} ↥(↑(↑(S i) : X.Opens) : Scheme)
Tactic: have : NoetherianSpace (S i) := by
        apply noetherianSpace_of_isAffineOpen (S i).1 (S i).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : Finite.{v + 1} 𝒰.I₀
inst_1 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
⊢ IsNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
have mp : IsNoetherian X → ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
have mpr : (∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)) → IsNoetherian X
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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₀
⊢ IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
have mp : IsLocallyNoetherian X
Tactic: apply (isLocallyNoetherian_iff_of_affine_openCover _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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
have mpr : IsLocallyNoetherian X
Tactic: convert! IsNoetherian.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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
⊢ IsNoetherian X
have mpr₁ : CompactSpace.{u} ↥X
Tactic: convert! IsNoetherian.mk
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
inst : IsNoetherian X
⊢ NoetherianSpace.{u_1} ↥X
have apply : NoetherianSpace.{u_1} (↑Set.univ : Type u_1)
Tactic: apply TopologicalSpace.noetherian_univ_iff.mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ NoetherianSpace.{u_1} (↑Set.univ : Type u_1)
have rw : NoetherianSpace.{u_1} (↑(⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)
Tactic: rw [← 𝒰.iUnion_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
⊢ NoetherianSpace.{u_1} (↑(⋃ (i : 𝒰.I₀), Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)
have suffices : ∀ (i : 𝒰.I₀), NoetherianSpace.{u_1} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)
Tactic: suffices ∀ i : 𝒰.I₀, NoetherianSpace (Set.range <| (𝒰.f i)) by
    apply NoetherianSpace.iUnion
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
⊢ IsAffine.{u_1} (𝒰.X i)
have rw : IsAffine.{u_1} (X.affineCover.X (Scheme.Cover.idx X.affineCover (↑i : ↥X)))
Tactic: rw [X.affineCover.finiteSubcover_X]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
X : Scheme
inst : IsNoetherian X
𝒰 : X.OpenCover := X.affineCover.finiteSubcover
i : 𝒰.I₀
⊢ NoetherianSpace.{u_1} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)
have this : IsAffine.{u_1} (𝒰.X i)
Tactic: have : IsAffine (𝒰.X i) := by
    rw [X.affineCover.finiteSubcover_X]
    apply Scheme.isAffine_affineCover
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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} (↑(Set.range (ι := ↥(𝒰.X i)) ⇑(𝒰.f i)) : Type u_1)
have convert! : IsNoetherianRing.{u_1} (↑Γ(X, (↑U : X.Opens)) : Type u_1)
Tactic: convert! noetherianSpace_of_isAffineOpen U.1 U.2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
⊢ IsNoetherian.{u_1} (Spec (CommRingCat.of R))
have suffices : IsNoetherianRing.{u_1} (↑(CommRingCat.of R) : Type u_1)
Tactic: suffices IsNoetherianRing (CommRingCat.of R) by infer_instance
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
inst : IsLocallyNoetherian X
x : ↥X
⊢ IsNoetherianRing.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
have 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)
Tactic: obtain ⟨U, hU, hU2, hU3⟩ := exists_isAffineOpen_mem_and_subset (U := ⊤) (x := x) (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
X : Scheme
inst : IsLocallyNoetherian X
x : ↥X
U : X.Opens
hU : IsAffineOpen U
hU2 : x ∈ U
hU3 : U.carrier ⊆ (↑⊤ : Set ↥X)
⊢ IsNoetherianRing.{u_1} (↑(X.presheaf.stalk x) : Type u_1)
have 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
Tactic: have := AlgebraicGeometry.IsAffineOpen.isLocalization_stalk hU ⟨x, hU2⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
V U : Y.Opensᵒᵖ
i : V ⟶ U
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)
hx :
  Membership.mem (γ := Subalgebra (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) x
⊢ Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop U) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop U) : Type u))
have obtain : ∀ (U : Y.Opens) (i : V ⟶ Opposite.op U),
  Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
Tactic: obtain ⟨U, rfl⟩ := Opposite.op_surjective U
Cleared hypotheses: U, i
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Normalization (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
V : Y.Opensᵒᵖ
x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)
hx :
  Membership.mem (γ := Subalgebra (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop V) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) x
U : Y.Opens
i : V ⟶ Opposite.op U
⊢ Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop V) : Type u)) → (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
have obtain : ∀ (V : Y.Opens) (x : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
  (hx :
    Membership.mem (γ :=
      Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
      (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op V)) : Type u)
        (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u))
      x)
  (i : Opposite.op V ⟶ Opposite.op U),
  Membership.mem (α := (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u)) (γ :=
    Subalgebra (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u) (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    (integralClosure (↑Γ(Y, Opposite.unop (Opposite.op U)) : Type u)
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
    ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE sorry).op) :
          (a : (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op V)) : Type u)) →
            (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
        x :
      (↑Γ(X, f ⁻¹ᵁ Opposite.unop (Opposite.op U)) : Type u))
Tactic: obtain ⟨V, rfl⟩ := Opposite.op_surjective V
Cleared hypotheses: V, x, hx, i