awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
h : HasPullback (Spec.map ψ) (Spec.map φ)
algInst : Algebra (↑K : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑K : Type u) (↑R : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
⊢ topologically @IsOpenMap (X := pullback (Spec.map ψ) (Spec.map φ)) (pullback.fst (Spec.map ψ) (Spec.map φ))

Tactic:
(MorphismProperty.cancel_left_of_respectsIso _ (pullbackSpecIso K R S).inv _).mp ?_

Premises used: CommRingCat.carrier, AlgebraicGeometry.pullbackSpecIso, Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
h : HasPullback (Spec.map ψ) (Spec.map φ)
algInst : Algebra (↑K : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑K : Type u) (↑R : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ topologically @IsOpenMap (X := pullback (Spec.map ψ) (Spec.map φ)) (pullback.fst (Spec.map ψ) (Spec.map φ))

Tactic:
refine (MorphismProperty.cancel_left_of_respectsIso _ (pullbackSpecIso K R S).inv _).mp ?_

Premises used: CommRingCat.carrier, AlgebraicGeometry.pullbackSpecIso, Iff.mp, CategoryTheory.MorphismProperty.cancel_left_of_respectsIso, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
h_1 : HasPullback (Spec.map ψ) (Spec.map φ)
algInst : Algebra (↑K : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑K : Type u) (↑R : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
h : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
convert_2 :
  topologically @IsOpenMap (X := Spec (CommRingCat.of (TensorProduct (↑K : Type u) (↑R : Type u) (↑S : Type u)))) (Y :=
    Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (TensorProduct (↑K : Type u) (↑R : Type u) (↑S : Type u)))))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
convert_to topologically _ (Spec.map <| CommRingCat.ofHom (algebraMap R (TensorProduct K R S)))

Premises used: CommRingCat.carrier, Algebra.algebraMap, CommRingCat.ofHom, AlgebraicGeometry.Spec.map, AlgebraicGeometry.topologically, TensorProduct
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
h : HasPullback (Spec.map ψ) (Spec.map φ)
algInst : Algebra (↑K : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑K : Type u) (↑R : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
e_3 : Spec R = Spec (CommRingCat.of (↑R : Type u))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
pullbackSpecIso_inv_fst ..

Premises used: Algebra.TensorProduct.includeLeftRingHom, AlgebraicGeometry.pullbackSpecIso_inv_fst, TensorProduct.tmul, AddCon.toQuotient
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
h : HasPullback (Spec.map ψ) (Spec.map φ)
algInst : Algebra (↑K : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑K : Type u) (↑R : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
e_3 : Spec R = Spec (CommRingCat.of (↑R : Type u))
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact pullbackSpecIso_inv_fst ..

Premises used: AlgebraicGeometry.pullbackSpecIso_inv_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
h : HasPullback (Spec.map ψ) (Spec.map φ)
algInst : Algebra (↑K : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑K : Type u) (↑R : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
this : Field (↑K : Type u) := hK.toField
⊢ topologically @IsOpenMap (X := Spec (CommRingCat.of (TensorProduct (↑K : Type u) (↑R : Type u) (↑S : Type u)))) (Y :=
    Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (TensorProduct (↑K : Type u) (↑R : Type u) (↑S : Type u)))))

Tactic:
PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field

Premises used: Set.Mem, setOf, PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field, AlgebraicGeometry.topologically, Quotient, TensorProduct, PrimeSpectrum.comap, AddCon.Quotient
-- Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
Goal:
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
h : HasPullback (Spec.map ψ) (Spec.map φ)
algInst : Algebra (↑K : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algInst_1 : Algebra (↑K : Type u) (↑R : Type u) := (CommRingCat.Hom.hom ψ).toAlgebra
this : Field (↑K : Type u) := hK.toField
⊢ topologically @IsOpenMap (X := Spec (CommRingCat.of (TensorProduct (↑K : Type u) (↑R : Type u) (↑S : Type u)))) (Y :=
    Spec (CommRingCat.of (↑R : Type u)))
    (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (TensorProduct (↑K : Type u) (↑R : Type u) (↑S : Type u)))))

Tactic:
exact PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field

Premises used: PrimeSpectrum.isOpenMap_comap_algebraMap_tensorProduct_of_field
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
h : ∀ (x x_1 : Scheme.{u}) (x_2 : x ⟶ x_1), WeaklyEtale x_2 ↔ (@Flat ⊓ MorphismProperty.diagonal @Flat) x_2
⊢ @WeaklyEtale = @Flat ⊓ MorphismProperty.diagonal @Flat

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ WeaklyEtale x_2 ↔ (@Flat ⊓ MorphismProperty.diagonal @Flat) x_2

Tactic:
weaklyEtale_iff _

Premises used: AlgebraicGeometry.weaklyEtale_iff, CategoryTheory.MorphismProperty.diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ WeaklyEtale x_2 ↔ (@Flat ⊓ MorphismProperty.diagonal @Flat) x_2

Tactic:
exact weaklyEtale_iff _

Premises used: AlgebraicGeometry.weaklyEtale_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (@Flat ⊓ MorphismProperty.diagonal @Flat).RespectsIso
⊢ MorphismProperty.RespectsIso @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Premises used: AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).RespectsIso

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (@Flat ⊓ MorphismProperty.diagonal @Flat).IsMultiplicative
⊢ MorphismProperty.IsMultiplicative @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Premises used: AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsMultiplicative

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : WeaklyEtale f
inst_1 : WeaklyEtale g
⊢ WeaklyEtale (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ f g inferInstance inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : (@Flat ⊓ MorphismProperty.diagonal @Flat).IsStableUnderBaseChange
⊢ MorphismProperty.IsStableUnderBaseChange @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Premises used: AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@Flat ⊓ MorphismProperty.diagonal @Flat).IsStableUnderBaseChange

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : IsZariskiLocalAtSource.{u_1} (@Flat ⊓ MorphismProperty.diagonal @Flat)
⊢ IsZariskiLocalAtSource @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Premises used: AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource.{u_1} (@Flat ⊓ MorphismProperty.diagonal @Flat)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : IsZariskiLocalAtTarget.{u_1} (@Flat ⊓ MorphismProperty.diagonal @Flat)
⊢ IsZariskiLocalAtTarget @WeaklyEtale

Tactic:
rw [weaklyEtale_eq_flat_inf_diagonal_flat]

Premises used: AlgebraicGeometry.WeaklyEtale.weaklyEtale_eq_flat_inf_diagonal_flat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget.{u_1} (@Flat ⊓ MorphismProperty.diagonal @Flat)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : WeaklyEtale g
⊢ WeaklyEtale (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : WeaklyEtale f
⊢ WeaklyEtale (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
V : Y.Opens
inst : WeaklyEtale f
⊢ WeaklyEtale (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g : Y ⟶ Z
f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : WeaklyEtale f
⊢ WeaklyEtale (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
rw : @WeaklyEtale ≤ MorphismProperty.diagonal @WeaklyEtale
⊢ MorphismProperty.HasOfPostcompProperty @WeaklyEtale @WeaklyEtale

Tactic:
rw [MorphismProperty.hasOfPostcompProperty_iff_le_diagonal]

Premises used: CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
hf : WeaklyEtale f
⊢ MorphismProperty.diagonal (@WeaklyEtale) f

Tactic:
inferInstanceAs <| WeaklyEtale (pullback.diagonal f)

Premises used: CategoryTheory.MorphismProperty.diagonal, AlgebraicGeometry.WeaklyEtale.instDiagonalScheme
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
hf : WeaklyEtale f
⊢ MorphismProperty.diagonal (@WeaklyEtale) f

Tactic:
exact inferInstanceAs <| WeaklyEtale (pullback.diagonal f)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : WeaklyEtale (f ≫ g)
inst_1 : WeaklyEtale g
⊢ WeaklyEtale f

Tactic:
MorphismProperty.of_postcomp _ _ g ‹_› ‹_›

Premises used: CategoryTheory.MorphismProperty.of_postcomp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
Goal:
⊢ @Etale ≤ @WeaklyEtale

Tactic:
fun _ _ _ _ ↦ inferInstance

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN : ∀ (s : ↥S), IsNoetherianRing.{u} (Localization.Away (↑s : R))
apply :
  ∀ (f : ℕ →o Submodule R R),
    ∃ (n : ℕ),
      ∀ (m : ℕ),
        n ≤ m →
          Eq (α := Submodule R R) ((f : (a : ℕ) → Submodule R R) n : Submodule R R)
            ((f : (a : ℕ) → Submodule R R) m : Submodule R R)
⊢ IsNoetherianRing R

Tactic:
apply monotone_stabilizes_iff_noetherian.mp

Premises used: monotone_stabilizes_iff_noetherian, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN : ∀ (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)
s : ↥S
h : (suitableN (↑s : R)).Nonempty
⊢ minN (↑s : R) ∈ suitableN (↑s : R)

Tactic:
apply Nat.sInf_mem

Premises used: Nat.sInf_mem
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN : ∀ (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)
s : ↥S
f : ℕ →o Ideal (Localization.Away (↑s : R)) :=
  {
    toFun := fun (n : ℕ) ↦
      Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (floc (↑s : R)) ((I : (a : ℕ) → Submodule R R) n),
    monotone' := ⋯ }
⊢ (suitableN (↑s : R)).Nonempty

Tactic:
monotone_stabilizes_iff_noetherian.mpr (hN s) f

Premises used: Iff.mpr, Set.Mem, setOf, Ideal.map, monotone_stabilizes_iff_noetherian, Set.Nonempty, Submodule.span
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN : ∀ (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)
s : ↥S
f : ℕ →o Ideal (Localization.Away (↑s : R)) :=
  {
    toFun := fun (n : ℕ) ↦
      Ideal.map (R := R) (F := R →+* Localization.Away (↑s : R)) (floc (↑s : R)) ((I : (a : ℕ) → Submodule R R) n),
    monotone' := ⋯ }
⊢ (suitableN (↑s : R)).Nonempty

Tactic:
exact monotone_stabilizes_iff_noetherian.mpr (hN s) f

Premises used: Iff.mpr, monotone_stabilizes_iff_noetherian
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN : ∀ (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)
⊢ ∀ (s : ↥S), minN (↑s : R) ∈ suitableN (↑s : R)

Tactic:
have hSuit : ∀ s : S, minN s ∈ suitableN s := by
    intro s
    apply Nat.sInf_mem
    let f : ℕ →o Ideal (Away (M := R) s) :=
      ⟨fun n ↦ Ideal.map (floc s) (I n), fun _ _ h ↦ Ideal.map_mono (I.monotone h)⟩
    exact monotone_stabilizes_iff_noetherian.mpr (hN s) f
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN : ∀ (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
h :
  ∀ (m : ℕ),
    N ≤ m →
      Eq (α := Submodule R R) ((I : (a : ℕ) → Submodule R R) N : Submodule R R)
        ((I : (a : ℕ) → Submodule R R) m : Submodule R R)
⊢ ∃ (n : ℕ),
    ∀ (m : ℕ),
      n ≤ m →
        Eq (α := Submodule R R) ((I : (a : ℕ) → Submodule R R) n : Submodule R R)
          ((I : (a : ℕ) → Submodule R R) m : Submodule R R)

Tactic:
use N
-- Module: Mathlib.AlgebraicGeometry.Noetherian
Goal:
R : Type u
inst : CommRing R
S : Finset R
hS : Eq (α := Ideal R) (Ideal.span (↑S : Set R)) ⊤
hN : ∀ (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
⊢ ∀ (s : ↥S), minN (↑s : R) ≤ N

Tactic:
have hN : ∀ s : S, minN s ≤ N := fun s => Finset.le_sup s.prop
-- 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
h :
  Eq.{u + 1} (α := Submodule R R)
    (⨅ (x : Subtype (Membership.mem S)),
      Ideal.under R (B := Localization.Away (↑x : R))
        (Ideal.map (R := R) (F := R →+* Localization.Away (↑x : R)) (algebraMap R (Localization.Away (↑x : R)))
          ((I : (a : ℕ) → Submodule R R) N)))
    (⨅ (x : Subtype (Membership.mem S)),
      Ideal.under R (B := Localization.Away (↑x : R))
        (Ideal.map (R := R) (F := R →+* Localization.Away (↑x : R)) (algebraMap R (Localization.Away (↑x : R)))
          ((I : (a : ℕ) → Submodule R R) n)))
⊢ Eq (α := Submodule R R) ((I : (a : ℕ) → Submodule R R) N : Submodule R R)
    ((I : (a : ℕ) → Submodule R R) n : Submodule R R)

Tactic:
rw [IsLocalization.ideal_eq_iInf_under_map_away hS (I N),
      IsLocalization.ideal_eq_iInf_under_map_away hS (I n),
      iInf_subtype', iInf_subtype']

Premises used: iInf_subtype', IsLocalization.ideal_eq_iInf_under_map_away, DFunLike.coe
-- 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
h :
  ∀ (i : Subtype (Membership.mem S)),
    Eq (α := Submodule R R)
      (Ideal.under R (B := Localization.Away (↑i : R))
        (Ideal.map (R := R) (F := R →+* Localization.Away (↑i : R)) (algebraMap R (Localization.Away (↑i : R)))
          ((I : (a : ℕ) → Submodule R R) N)))
      (Ideal.under R (B := Localization.Away (↑i : R))
        (Ideal.map (R := R) (F := R →+* Localization.Away (↑i : R)) (algebraMap R (Localization.Away (↑i : R)))
          ((I : (a : ℕ) → Submodule R R) n)))
⊢ Eq.{u + 1} (α := Submodule R R)
    (⨅ (x : Subtype (Membership.mem S)),
      Ideal.under R (B := Localization.Away (↑x : R))
        (Ideal.map (R := R) (F := R →+* Localization.Away (↑x : R)) (algebraMap R (Localization.Away (↑x : R)))
          ((I : (a : ℕ) → Submodule R R) N)))
    (⨅ (x : Subtype (Membership.mem S)),
      Ideal.under R (B := Localization.Away (↑x : R))
        (Ideal.map (R := R) (F := R →+* Localization.Away (↑x : R)) (algebraMap R (Localization.Away (↑x : R)))
          ((I : (a : ℕ) → Submodule R R) n)))

Tactic:
apply iInf_congr

Premises used: iInf_congr