awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
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))
⊢ 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)))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
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))
⊢ 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:
rw [← hSuit s N (hN s)]
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)) (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:
hSuit s n <| Nat.le_trans (hN s) hn

Premises used: Set.Mem, Nat.le_trans
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)) (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:
exact hSuit s n <| Nat.le_trans (hN s) hn

Premises used: Nat.le_trans
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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

Tactic:
⟨fun U => ?_⟩

Premises used: AlgebraicGeometry.IsLocallyNoetherian.mk
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
refine : ∀ (U : (↑X.affineOpens : Type u_2)), IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)
⊢ IsLocallyNoetherian X

Tactic:
refine ⟨fun U => ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_2)

Tactic:
have := U.prop.isLocalization_basicOpen f
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_2)
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u_2)

Tactic:
IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN

Premises used: CommRingCat.carrier, IsLocalization.isNoetherianRing, AlgebraicGeometry.RingedSpace.basicOpen, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_2)
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑(X.affineBasicOpen f) : X.Opens)) : Type u_2)

Tactic:
exact IsLocalization.isNoetherianRing (.powers f) Γ(X, X.basicOpen f) hN

Premises used: CommRingCat.carrier, IsLocalization.isNoetherianRing, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
openCover : ∀ (s_1 : ↥s), IsNoetherianRing.{u_2} (Localization.Away (↑s_1 : (↑Γ(X, (↑U : X.Opens)) : Type u_2)))
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑U : X.Opens)) : Type u_2)

Tactic:
apply isNoetherianRing_of_away s ‹_›

Premises used: AlgebraicGeometry.isNoetherianRing_of_away
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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} (↑Γ(X, X.basicOpen f) : Type u_2)

Tactic:
have : IsNoetherianRing Γ(X, X.basicOpen f) := hN ⟨f, hf⟩
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u_2)

Tactic:
have := U.prop.isLocalization_basicOpen f
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
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)))
⊢ 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)
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
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:
isNoetherianRing_of_ringEquiv Γ(X, X.basicOpen f) hEq.symm.toRingEquiv

Premises used: CommRingCat.carrier, AlgEquiv.symm, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, AlgEquiv.toRingEquiv, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, isNoetherianRing_of_ringEquiv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
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:
exact isNoetherianRing_of_ringEquiv Γ(X, X.basicOpen f) hEq.symm.toRingEquiv

Premises used: CommRingCat.carrier, AlgEquiv.symm, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.Scheme.basicOpen, AlgEquiv.toRingEquiv, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, isNoetherianRing_of_ringEquiv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
i : ι
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)

Tactic:
hS' _
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
i : ι
⊢ IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)

Tactic:
exact hS' _
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
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)
hU : ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : 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' _
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
X : Scheme
ι : Sort u_1
S : ι → (↑X.affineOpens : Type u_2)
hS : Eq.{u_2 + 1} (α := X.Opens) (⨆ (i : ι), (↑(S i) : X.Opens)) ⊤
⊢ IsLocallyNoetherian X ↔ ∀ (i : ι), IsNoetherianRing.{u_2} (↑Γ(X, (↑(S i) : X.Opens)) : Type u_2)

Tactic:
⟨fun _ i => IsLocallyNoetherian.component_noetherian (S i),
   isLocallyNoetherian_of_affine_cover hS⟩

Premises used: AlgebraicGeometry.isLocallyNoetherian_of_affine_cover, Iff.intro, AlgebraicGeometry.IsLocallyNoetherian.component_noetherian
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
mpr : (∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)) → IsLocallyNoetherian X
⊢ IsLocallyNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)

Tactic:
constructor
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) U ⋯) : X.Opens)) : Type u)

Tactic:
have := h.component_noetherian ⟨U, isAffineOpen_opensRange _⟩
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
mp : (↑Γ(X, U) : Type u) ≃+* (↑Γ(𝒰.X i, ⊤) : Type u)
⊢ IsNoetherianRing.{u} (↑Γ(𝒰.X i, ⊤) : Type u)

Tactic:
apply isNoetherianRing_of_ringEquiv (R := Γ(X, U))

Premises used: CommRingCat.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, CategoryTheory.Functor.obj, isNoetherianRing_of_ringEquiv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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)
mp : Γ(X, U) ≅ Γ(𝒰.X i, ⊤)
⊢ (↑Γ(X, U) : Type u) ≃+* (↑Γ(𝒰.X i, ⊤) : Type u)

Tactic:
apply CategoryTheory.Iso.commRingCatIsoToRingEquiv

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv
-- Module: Mathlib.AlgebraicGeometry.Noetherian
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) ≅ Γ(𝒰.X i, ⊤)

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

Premises used: CategoryTheory.PreZeroHypercover.f, AlgebraicGeometry.IsOpenImmersion.ΓIsoTop, CategoryTheory.Iso.symm, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- 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)) ⋯
mpr : Eq.{u + 1} (α := X.Opens) (⨆ (i : 𝒰.I₀), (↑(fS i) : X.Opens)) ⊤
mpr₁ : ∀ (i : 𝒰.I₀), IsNoetherianRing.{u} (↑Γ(X, (↑(fS i) : X.Opens)) : Type u)
⊢ IsLocallyNoetherian X

Tactic:
apply isLocallyNoetherian_of_affine_cover (S := fS)

Premises used: AlgebraicGeometry.isLocallyNoetherian_of_affine_cover
-- 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)) ⋯
mpr mpr₁ : Eq.{u + 1} (α := X.Opens) (⨆ (i : 𝒰.I₀), (↑(fS i) : X.Opens)) (⨆ (i : 𝒰.I₀), Scheme.Hom.opensRange (𝒰.f i))
⊢ Eq.{u + 1} (α := X.Opens) (⨆ (i : 𝒰.I₀), (↑(fS i) : X.Opens)) ⊤

Tactic:
rw [← Scheme.OpenCover.iSup_opensRange 𝒰]

Premises used: AlgebraicGeometry.Scheme.OpenCover.iSup_opensRange
-- 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₀
mpr : (↑Γ(𝒰.X i, ⊤) : Type u) ≃+* (↑Γ(X, (↑(fS i) : X.Opens)) : Type u)
⊢ IsNoetherianRing.{u} (↑Γ(X, (↑(fS i) : X.Opens)) : Type u)

Tactic:
apply isNoetherianRing_of_ringEquiv (R := Γ(𝒰.X i, ⊤))

Premises used: CommRingCat.carrier, CategoryTheory.PreZeroHypercover.X, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Top.top, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover, CategoryTheory.Functor.obj, isNoetherianRing_of_ringEquiv, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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₀
mpr : Γ(𝒰.X i, ⊤) ≅ Γ(X, (↑(fS i) : X.Opens))
⊢ (↑Γ(𝒰.X i, ⊤) : Type u) ≃+* (↑Γ(X, (↑(fS i) : X.Opens)) : Type u)

Tactic:
apply CategoryTheory.Iso.commRingCatIsoToRingEquiv

Premises used: CategoryTheory.Iso.commRingCatIsoToRingEquiv