awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN_1 : ∀ (s : ↥S), IsNoetherianRing.{u} (Localization.Away (↑s : R))
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun (s : R) ↦ algebraMap R (Localization.Away s)
suitableN : (s : R) → Set ℕ :=
  fun (s : R) ↦
    {n : ℕ |
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Ideal (Localization.Away s)) (Ideal.map (R := R) (floc s) ((I : (a : ℕ) → Submodule R R) n))
            (Ideal.map (R := R) (floc s) ((I : (a : ℕ) → Submodule R R) m))}
minN : (s : R) → ℕ := fun (s : R) ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN (↑s : R) ∈ suitableN (↑s : R)
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN (↑s : R) ≤ N
n : ℕ
hn : N ≤ n
s : Subtype (Membership.mem S)
⊢ Eq (α := Submodule R R)
    (Ideal.under R (B := Localization.Away (↑s : R))
      (Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (algebraMap R (Localization.Away (↑s : R)))
        ((I : (a : ℕ) → Submodule R R) N)))
    (Ideal.under R (B := Localization.Away (↑s : R))
      (Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (algebraMap R (Localization.Away (↑s : R)))
        ((I : (a : ℕ) → Submodule R R) n)))
have h : Eq (α := Ideal (Localization.Away (↑s : R)))
  (Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (algebraMap R (Localization.Away (↑s : R)))
    ((I : (a : ℕ) → Submodule R R) N))
  (Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (algebraMap R (Localization.Away (↑s : R)))
    ((I : (a : ℕ) → Submodule R R) n))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN_1 : ∀ (s : ↥S), IsNoetherianRing.{u} (Localization.Away (↑s : R))
I : ℕ →o Submodule R R
floc : (s : R) → R →+* Localization.Away s := fun (s : R) ↦ algebraMap R (Localization.Away s)
suitableN : (s : R) → Set ℕ :=
  fun (s : R) ↦
    {n : ℕ |
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Ideal (Localization.Away s)) (Ideal.map (R := R) (floc s) ((I : (a : ℕ) → Submodule R R) n))
            (Ideal.map (R := R) (floc s) ((I : (a : ℕ) → Submodule R R) m))}
minN : (s : R) → ℕ := fun (s : R) ↦ sInf (suitableN s)
hSuit : ∀ (s : ↥S), minN (↑s : R) ∈ suitableN (↑s : R)
N : ℕ := S.sup minN
hN : ∀ (s : ↥S), minN (↑s : R) ≤ N
n : ℕ
hn : N ≤ n
s : Subtype (Membership.mem S)
⊢ Eq (α := Ideal (Localization.Away (↑s : R)))
    (Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (algebraMap R (Localization.Away (↑s : R)))
      ((I : (a : ℕ) → Submodule R R) N))
    (Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (algebraMap R (Localization.Away (↑s : R)))
      ((I : (a : ℕ) → Submodule R R) n))
have h : Eq (α := Ideal (Localization.Away (↑s : R)))
  (Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (floc (↑s : R))
    ((I : (a : ℕ) → Submodule R R) (minN (↑s : R))))
  (Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (algebraMap R (Localization.Away (↑s : R)))
    ((I : (a : ℕ) → Submodule R R) n))
Tactic: rw [← hSuit s N (hN s)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
hS' : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
⊢ IsLocallyNoetherian X
have refine : ∀ (U : (↑X.affineOpens : Type u_2)), IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)
Tactic: refine ⟨fun U => ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
hS' : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
U : (↑X.affineOpens : Type u_2)
f : (↑Γ(X, (↑U : X.Opens)) : Type u_2)
hN : IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u_2)
have this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_2)
Tactic: have := U.prop.isLocalization_basicOpen f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
hS' : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
U : (↑X.affineOpens : Type u_2)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_2)
h : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_2)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_2))) ⊤
hN :
  ∀ (f : ↥s),
    IsNoetherianRing.{u_2}
      (↑Γ(X, (↑(X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_2))) : X.Opens)) : Type u_2)
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)
have openCover : ∀ (s_1 : ↥s), IsNoetherianRing.{u_2} (Localization.Away (↑s_1 : (↑Γ(X, (↑U : X.Opens)) : Type u_2)))
Tactic: apply isNoetherianRing_of_away s ‹_›
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
hS' : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
U : (↑X.affineOpens : Type u_2)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_2)
h : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_2)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_2))) ⊤
hN :
  ∀ (f : ↥s),
    IsNoetherianRing.{u_2}
      (↑Γ(X, (↑(X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_2))) : X.Opens)) : Type u_2)
f : (↑Γ(X, (↑U : X.Opens)) : Type u_2)
hf : f ∈ s
⊢ IsNoetherianRing.{u_2}
    (Localization.Away
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u_2)) ↦ x ∈ s) f hf) :
        (↑Γ(X, (↑U : X.Opens)) : Type u_2)))
have this : IsNoetherianRing.{u_2} (↑Γ(X, X.basicOpen f) : Type u_2)
Tactic: have : IsNoetherianRing Γ(X, X.basicOpen f) := hN ⟨f, hf⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
hS' : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
U : (↑X.affineOpens : Type u_2)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_2)
h : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_2)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_2))) ⊤
hN :
  ∀ (f : ↥s),
    IsNoetherianRing.{u_2}
      (↑Γ(X, (↑(X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_2))) : X.Opens)) : Type u_2)
f : (↑Γ(X, (↑U : X.Opens)) : Type u_2)
hf : f ∈ s
this : IsNoetherianRing.{u_2} (↑Γ(X, X.basicOpen f) : Type u_2)
⊢ IsNoetherianRing.{u_2}
    (Localization.Away
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u_2)) ↦ x ∈ s) f hf) :
        (↑Γ(X, (↑U : X.Opens)) : Type u_2)))
have this₁ : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_2)
Tactic: have := U.prop.isLocalization_basicOpen f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
hS' : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
U : (↑X.affineOpens : Type u_2)
s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_2)
h : Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_2)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_2))) ⊤
hN :
  ∀ (f : ↥s),
    IsNoetherianRing.{u_2}
      (↑Γ(X, (↑(X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_2))) : X.Opens)) : Type u_2)
f : (↑Γ(X, (↑U : X.Opens)) : Type u_2)
hf : f ∈ s
this_1 : IsNoetherianRing.{u_2} (↑Γ(X, X.basicOpen f) : Type u_2)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_2)
⊢ IsNoetherianRing.{u_2}
    (Localization.Away
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u_2)) ↦ x ∈ s) f hf) :
        (↑Γ(X, (↑U : X.Opens)) : Type u_2)))
have openCover : ∀ (hEq : Localization.Away f ≃ₐ[(↑Γ(X, (↑U : X.Opens)) : Type u_2)] (↑Γ(X, X.basicOpen f) : Type u_2)),
  IsNoetherianRing.{u_2}
    (Localization.Away
      (↑(Subtype.mk (p := fun (x : (↑Γ(X, (↑U : X.Opens)) : Type u_2)) ↦ x ∈ s) f hf) :
        (↑Γ(X, (↑U : X.Opens)) : Type u_2)))
Tactic: have hEq := IsLocalization.algEquiv (.powers f) (Localization.Away f) Γ(X, X.basicOpen f)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
hS' : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
U : (↑X.affineOpens : Type u_2)
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)
have basicOpen : ∀ (U : (↑X.affineOpens : Type u_2)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_2))
  (hN : IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)),
  IsNoetherianRing.{u_2} (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u_2)
Tactic: induction U using of_affine_open_cover S hS with
  | basicOpen U f hN =>
    have := U.prop.isLocalization_basicOpen f
    exact IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN
  | openCover U s _ hN =>
    apply isNoetherianRing_of_away s ‹_›
    intro ⟨f, hf⟩
    have : IsNoetherianRing Γ(X, X.basicOpen f) := hN ⟨f, hf⟩
    have := U.prop.isLocalization_basicOpen f
    have hEq := IsLocalization.algEquiv (.powers f) (Localization.Away f) Γ(X, X.basicOpen f)
    exact isNoetherianRing_of_ringEquiv Γ(X, X.basicOpen f) hEq.symm.toRingEquiv
  | hU => exact hS' _
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
hS' : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)
U : (↑X.affineOpens : Type u_2)
basicOpen :
  ∀ (U : (↑X.affineOpens : Type u_2)) (f : (↑Γ(X, (↑U : X.Opens)) : Type u_2))
    (hN : IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)),
    IsNoetherianRing.{u_2} (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u_2)
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)
have openCover : ∀ (U : (↑X.affineOpens : Type u_2)) (s : Finset (↑Γ(X, (↑U : X.Opens)) : Type u_2)),
  Eq (α := Ideal (↑Γ(X, (↑U : X.Opens)) : Type u_2)) (Ideal.span (↑s : Set (↑Γ(X, (↑U : X.Opens)) : Type u_2))) ⊤ →
    ∀
      (hN :
        ∀ (f : ↥s),
          IsNoetherianRing.{u_2}
            (↑Γ(X, (↑(X.affineBasicOpen (↑f : (↑Γ(X, (↑U : X.Opens)) : Type u_2))) : X.Opens)) : Type u_2)),
      IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)
Tactic: induction U using of_affine_open_cover S hS with
  | basicOpen U f hN =>
    have := U.prop.isLocalization_basicOpen f
    exact IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN
  | openCover U s _ hN =>
    apply isNoetherianRing_of_away s ‹_›
    intro ⟨f, hf⟩
    have : IsNoetherianRing Γ(X, X.basicOpen f) := hN ⟨f, hf⟩
    have := U.prop.isLocalization_basicOpen f
    have hEq := IsLocalization.algEquiv (.powers f) (Localization.Away f) Γ(X, X.basicOpen f)
    exact isNoetherianRing_of_ringEquiv Γ(X, X.basicOpen f) hEq.symm.toRingEquiv
  | hU => exact hS' _
Cleared hypotheses: U
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
have mp : IsLocallyNoetherian 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 : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
mp : IsLocallyNoetherian X → ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
have mpr : (∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)) → IsLocallyNoetherian X
Tactic: constructor
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
h : IsLocallyNoetherian X
i : 𝒰.I₀
U : X.Opens := Scheme.Hom.opensRange (𝒰.f i)
⊢ IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
have this : IsNoetherianRing.{u} (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U sorry) : X.Opens)) : Type u)
Tactic: have := h.component_noetherian ⟨U, isAffineOpen_opensRange _⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
h : IsLocallyNoetherian X
i : 𝒰.I₀
U : X.Opens := Scheme.Hom.opensRange (𝒰.f i)
this : IsNoetherianRing.{u} (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U ⋯) : X.Opens)) : Type u)
⊢ IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)
have mp : (↑Γ(X, U) : Type u) ≃+* (↑Γ(𝒰.X i, ⊤) : Type u)
Tactic: apply isNoetherianRing_of_ringEquiv (R := Γ(X, U))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{v, u} X
inst : ∀ (i : 𝒰.I₀), IsAffine.{u} (𝒰.X i)
h : IsLocallyNoetherian X
i : 𝒰.I₀
U : X.Opens := Scheme.Hom.opensRange (𝒰.f i)
this : IsNoetherianRing.{u} (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U ⋯) : X.Opens)) : Type u)
⊢ (↑Γ(X, U) : Type u) ≃+* (↑Γ(𝒰.X i, ⊤) : Type u)
have mp : Γ(X, U) ≅ Γ(𝒰.X i, ⊤)
Tactic: apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)) ⋯
⊢ IsLocallyNoetherian X
have mpr : Eq.{u + 1} (α := X.Opens) (⨆ (i : 𝒰.I₀), (↑(fS i) : X.Opens)) ⊤
Tactic: apply isLocallyNoetherian_of_affine_cover (S := fS)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)) ⋯
mpr : Eq.{u + 1} (α := X.Opens) (⨆ (i : 𝒰.I₀), (↑(fS i) : X.Opens)) ⊤
⊢ IsLocallyNoetherian X
have mpr₁ : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(X, (↑(fS i) : X.Opens)) : Type u)
Tactic: apply isLocallyNoetherian_of_affine_cover (S := fS)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)) ⋯
⊢ Eq.{u + 1} (α := X.Opens) (⨆ (i : 𝒰.I₀), (↑(fS i) : X.Opens)) ⊤
have mpr : Eq.{u + 1} (α := X.Opens) (⨆ (i : 𝒰.I₀), (↑(fS i) : X.Opens)) (⨆ (i : 𝒰.I₀), Scheme.Hom.opensRange (𝒰.f i))
Tactic: rw [← Scheme.OpenCover.iSup_opensRange 𝒰]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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₀
⊢ IsNoetherianRing.{u} (↑Γ(X, (↑(fS i) : X.Opens)) : Type u)
have mpr : (↑Γ(𝒰.X i, ⊤) : Type u) ≃+* (↑Γ(X, (↑(fS i) : X.Opens)) : Type u)
Tactic: apply isNoetherianRing_of_ringEquiv (R := Γ(𝒰.X i, ⊤))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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, ⊤) : Type u) ≃+* (↑Γ(X, (↑(fS i) : X.Opens)) : Type u)
have mpr : Γ(𝒰.X i, ⊤) ≅ Γ(X, (↑(fS i) : X.Opens))
Tactic: apply CategoryTheory.Iso.commRingCatIsoToRingEquiv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)
have refine : (∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)) → IsLocallyNoetherian X
Tactic: refine ⟨fun _ ↦ inferInstance, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
𝒰 : Scheme.OpenCover.{u_1, u_2} X
⊢ (∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)) → IsLocallyNoetherian X
have rw : (∀ (i : 𝒰.I₀), IsLocallyNoetherian.{u_2} (𝒰.X i)) →
  ∀ (i : 𝒰.affineRefinement.openCover.I₀), IsNoetherianRing.{u_2} (↑Γ(𝒰.affineRefinement.openCover.X i, ⊤) : Type u_2)
Tactic: rw [isLocallyNoetherian_iff_of_affine_openCover (𝒰 := 𝒰.affineRefinement.openCover)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
inst : IsNoetherianRing.{u_1} (↑Γ(X, U) : Type u_1)
⊢ NoetherianSpace.{u_1} ↥(↑U : Scheme)
have this : IsNoetherianRing.{u_1} (↑Γ((↑U : Scheme), ⊤) : Type u_1)
Tactic: have : IsNoetherianRing Γ(U, ⊤) := isNoetherianRing_of_ringEquiv _
    (Scheme.restrictFunctorΓ.app (op U)).symm.commRingCatIsoToRingEquiv
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
⊢ QuasiCompact f
have apply : ∀ (U : X.Opens), IsAffineOpen U → IsCompact (↑(f ⁻¹ᵁ U) : Set ↥Z)
Tactic: apply quasiCompact_iff_forall_isAffineOpen.mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (↑(f ⁻¹ᵁ U) : Set ↥Z)
have rw : IsCompact (X := ↥Z) (⇑f ⁻¹' ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f))
Tactic: rw [Opens.map_coe, ← Set.preimage_inter_range]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact (X := ↥Z) (⇑f ⁻¹' ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f))
have hK : IsCompact ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f)
Tactic: apply f.isOpenEmbedding.isInducing.isCompact_preimage'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsCompact (X := ↥Z) (⇑f ⁻¹' ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f))
have Kf : (↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f ⊆ Set.range (ι := ↥Z) ⇑f
Tactic: apply f.isOpenEmbedding.isInducing.isCompact_preimage'
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ IsCompact ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f)
have hK : NoetherianSpace.{u_1} (↑(↑U : Set ↥X) : Type u_1)
Tactic: apply (noetherianSpace_set_iff _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsCompact ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f)
have hK₁ : (↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f ⊆ (↑U : Set ↥X)
Tactic: apply (noetherianSpace_set_iff _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
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)
⊢ IsCompact ((↑U : Set ↥X) ∩ Set.range (ι := ↥Z) ⇑f)
have apply : Set ↥X
Tactic: apply (noetherianSpace_set_iff _).mp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X Z : Scheme
inst : IsLocallyNoetherian X
f : Z ⟶ X
inst_1 : IsOpenImmersion f
U : X.Opens
hU : IsAffineOpen U
⊢ NoetherianSpace.{u_1} (↑(↑U : Set ↥X) : Type u_1)
have hK : IsNoetherianRing.{u_1} (↑Γ(X, U) : Type u_1)
Tactic: convert! noetherianSpace_of_isAffineOpen U hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (goal)
Goal:
X : Scheme
inst : IsLocallyNoetherian X
⊢ QuasiSeparatedSpace.{u_1} ↥X
have apply : ∀ (U V : (↑X.affineOpens : Type u_1)), IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
Tactic: apply quasiSeparatedSpace_iff_forall_affineOpens.mpr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
Goal:
X : Scheme
inst : IsLocallyNoetherian X
U V : (↑X.affineOpens : Type u_1)
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have hInd : Topology.IsInducing (X := ↥(Spec Γ(X, (↑U : X.Opens)))) (Y := ↥X) ⇑(IsAffineOpen.fromSpec sorry)
Tactic: have hInd := U.2.fromSpec.isOpenEmbedding.isInducing
-- 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) ∩ (↑(↑V : X.Opens) : Set ↥X))
have apply : IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
  (⇑(IsAffineOpen.fromSpec sorry) ⁻¹' ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
Tactic: apply (hInd.isCompact_preimage_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 ⋯)
apply :
  IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
    (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
⊢ IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))
have apply₁ : (↑(↑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_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 ⋯)
⊢ IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
    (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
have rw : IsCompact (X := ↥(Spec Γ(X, (↑U : X.Opens))))
  (⇑(IsAffineOpen.fromSpec sorry) ⁻¹'
    ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))))
Tactic: rw [← Set.preimage_inter_range, IsAffineOpen.range_fromSpec, Set.inter_comm]
-- 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 (X := ↥(Spec Γ(X, (↑U : X.Opens))))
    (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹'
      ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X))))
have hK : IsCompact ((↑(↑U : X.Opens) : Set ↥X) ∩ ((↑(↑U : X.Opens) : Set ↥X) ∩ (↑(↑V : X.Opens) : Set ↥X)))
Tactic: apply hInd.isCompact_preimage'