awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
inr :
  ∀ (this : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f)
    (hX : ¬∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f
⊢ UniversallyOpen f
have wlog : ∀ {X : Scheme.{u}} (f : X ⟶ Y) (hX : ∃ (S : CommRingCat.{u}), X = Spec S), UniversallyOpen f
Tactic: wlog hX : ∃ S, X = Spec S generalizing X
Cleared hypotheses: X, f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
X : Scheme
f : X ⟶ Y
hX : ∃ (S : CommRingCat.{u}), X = Spec S
⊢ UniversallyOpen f
have obtain : ∀ (S : CommRingCat.{u}) (f : Spec S ⟶ Y), UniversallyOpen f
Tactic: obtain ⟨S, rfl⟩ := hX
Cleared hypotheses: X, f, hX
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
S : CommRingCat
f : Spec S ⟶ Y
⊢ UniversallyOpen f
have inr : ∀
  (this :
    ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
      (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f)
  (hY : ¬∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
Tactic: wlog hY : ∃ K, Y = Spec K ∧ IsField K generalizing Y
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
S : CommRingCat
f : Spec S ⟶ Y
inr :
  ∀
    (this :
      ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
        (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f)
    (hY : ¬∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
⊢ UniversallyOpen f
have wlog : ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
  (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
Tactic: wlog hY : ∃ K, Y = Spec K ∧ IsField K generalizing Y
Cleared hypotheses: Y, inst, inst_1, f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (hypothesis)
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme.{u}} [IsIntegral Y] [Subsingleton.{u + 1} ↥Y] (f : Spec S ⟶ Y)
    (hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)), UniversallyOpen f
hY : ¬∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)
⊢ UniversallyOpen f
have inst : Subsingleton.{u + 1} ↥(Spec Γ(Y, ⊤))
Tactic: have inst : Subsingleton (Spec Γ(Y, ⊤)) := Y.isoSpec.inv.homeomorph.subsingleton
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y_1 : Scheme
f_1 : X ⟶ Y_1
S : CommRingCat
Y : Scheme
inst : IsIntegral Y
inst_1 : Subsingleton.{u + 1} ↥Y
f : Spec S ⟶ Y
hY : ∃ (K : CommRingCat.{u}), Y = Spec K ∧ IsField.{u} (↑K : Type u)
⊢ UniversallyOpen f
have obtain : ∀ (K : CommRingCat.{u}) (hK : IsField.{u} (↑K : Type u)) [IsIntegral.{u} (Spec K)] [Subsingleton.{u + 1} ↥(Spec K)]
  (f : Spec S ⟶ Spec K), UniversallyOpen f
Tactic: obtain ⟨K, rfl, hK⟩ := hY
Cleared hypotheses: Y, inst, inst_1, f, hY
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
S K : CommRingCat
hK : IsField.{u} (↑K : Type u)
inst : IsIntegral.{u} (Spec K)
inst_1 : Subsingleton.{u + 1} ↥(Spec K)
f : Spec S ⟶ Spec K
⊢ UniversallyOpen f
have obtain : ∀ (φ : K ⟶ S), UniversallyOpen (Spec.map φ)
Tactic: obtain ⟨φ, rfl⟩ := Spec.map_surjective f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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
⊢ UniversallyOpen (Spec.map φ)
have refine : ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
  topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
Tactic: refine ⟨universally_mk' _ _ fun {T} g _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
have inr : ∀
  (this :
    ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
      topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)))
  (hT : ¬∃ (R : CommRingCat.{u}), T = Spec R),
  topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
Tactic: wlog hT : ∃ R, T = Spec R generalizing T
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
inr :
  ∀
    (this :
      ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
        topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)))
    (hT : ¬∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
have wlog : ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
  topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
Tactic: wlog hT : ∃ R, T = Spec R generalizing T
Cleared hypotheses: T, g, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
have inr : ∀ (i : T.affineCover.toPreZeroHypercover.1),
  topologically @IsOpenMap (X :=
    PreZeroHypercover.X (S := pullback g (Spec.map φ))
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) T.affineCover (pullback.fst g (Spec.map φ)) i :
      PreZeroHypercover.X (S := pullback g (Spec.map φ))
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
          i ⟶
        T.affineCover.X i)
Tactic: refine (IsZariskiLocalAtTarget.iff_of_openCover T.affineCover).mpr fun i ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme.{u}} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)) (hT : ∃ (R : CommRingCat.{u}), T = Spec R),
    topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
hT : ¬∃ (R : CommRingCat.{u}), T = Spec R
i : T.affineCover.toPreZeroHypercover.1
⊢ topologically @IsOpenMap (X :=
    PreZeroHypercover.X (S := pullback g (Spec.map φ))
      (Precoverage.ZeroHypercover.toPreZeroHypercover
        (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
      i)
    (Scheme.Cover.pullbackHom (P := IsOpenImmersion) T.affineCover (pullback.fst g (Spec.map φ)) i :
      PreZeroHypercover.X (S := pullback g (Spec.map φ))
          (Precoverage.ZeroHypercover.toPreZeroHypercover
            (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
          i ⟶
        T.affineCover.X i)
have inr : topologically @IsOpenMap (X := pullback (T.affineCover.f i ≫ g) (Spec.map φ))
  (CategoryStruct.comp (Y := pullback (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)) (T.affineCover.f i))
      (CategoryStruct.comp (Y :=
          pullback (Y := pullback g (Spec.map φ)) (T.affineCover.f i) (pullback.fst g (Spec.map φ)))
          (Iso.inv (pullbackRightPullbackFstIso g (Spec.map φ) (T.affineCover.f i)))
          (Iso.hom (pullbackSymmetry (T.affineCover.f i) (pullback.fst g (Spec.map φ)))) :
        pullback (T.affineCover.f i ≫ g) (Spec.map φ) ⟶
          pullback (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ)) (T.affineCover.f i))
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) T.affineCover (pullback.fst g (Spec.map φ)) i :
        PreZeroHypercover.X (S := pullback g (Spec.map φ))
            (Precoverage.ZeroHypercover.toPreZeroHypercover
              (Precoverage.ZeroHypercover.pullback₁ (pullback.fst g (Spec.map φ)) T.affineCover))
            i ⟶
          T.affineCover.X i) :
    pullback (T.affineCover.f i ≫ g) (Spec.map φ) ⟶ T.affineCover.X i)
Tactic: refine (MorphismProperty.cancel_left_of_respectsIso _
      ((pullbackRightPullbackFstIso ..).inv ≫ (pullbackSymmetry ..).hom) _).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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
T : Scheme
g : T ⟶ Spec K
h : HasPullback g (Spec.map φ)
hT : ∃ (R : CommRingCat.{u}), T = Spec R
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
have obtain : ∀ (R : CommRingCat.{u}) (g : Spec R ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
  topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
Tactic: obtain ⟨R, rfl⟩ := hT
Cleared hypotheses: T, g, h, hT
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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
g : Spec R ⟶ Spec K
h : HasPullback g (Spec.map φ)
⊢ topologically @IsOpenMap (X := pullback g (Spec.map φ)) (pullback.fst g (Spec.map φ))
have obtain : ∀ (ψ : K ⟶ R) (x : HasPullback (Spec.map ψ) (Spec.map φ)),
  topologically @IsOpenMap (X := pullback (Spec.map ψ) (Spec.map φ)) (pullback.fst (Spec.map ψ) (Spec.map φ))
Tactic: obtain ⟨ψ, rfl⟩ := Spec.map_surjective g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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 φ))
have refine : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: refine (MorphismProperty.cancel_left_of_respectsIso _ (pullbackSpecIso K R S).inv _).mp ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have h : 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)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen (goal)
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)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
have 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)))))
Tactic: convert_to topologically _ (Spec.map <| CommRingCat.ofHom (algebraMap R (TensorProduct K R S)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale (goal)
Goal:
⊢ @WeaklyEtale = @Flat ⊓ MorphismProperty.diagonal @Flat
have h : ∀ (x x_1 : Scheme.{u}) (x_2 : x ⟶ x_1), WeaklyEtale x_2 ↔ (@Flat ⊓ MorphismProperty.diagonal @Flat) x_2
Tactic: ext
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @WeaklyEtale
have rw : (@Flat ⊓ MorphismProperty.diagonal @Flat).RespectsIso
Tactic: rw [weaklyEtale_eq_flat_inf_diagonal_flat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsMultiplicative @WeaklyEtale
have rw : (@Flat ⊓ MorphismProperty.diagonal @Flat).IsMultiplicative
Tactic: rw [weaklyEtale_eq_flat_inf_diagonal_flat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @WeaklyEtale
have rw : (@Flat ⊓ MorphismProperty.diagonal @Flat).IsStableUnderBaseChange
Tactic: rw [weaklyEtale_eq_flat_inf_diagonal_flat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource @WeaklyEtale
have rw : IsZariskiLocalAtSource.{u_1} (@Flat ⊓ MorphismProperty.diagonal @Flat)
Tactic: rw [weaklyEtale_eq_flat_inf_diagonal_flat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @WeaklyEtale
have rw : IsZariskiLocalAtTarget.{u_1} (@Flat ⊓ MorphismProperty.diagonal @Flat)
Tactic: rw [weaklyEtale_eq_flat_inf_diagonal_flat]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale (goal)
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.HasOfPostcompProperty @WeaklyEtale @WeaklyEtale
have rw : @WeaklyEtale ≤ MorphismProperty.diagonal @WeaklyEtale
Tactic: rw [MorphismProperty.hasOfPostcompProperty_iff_le_diagonal]
-- 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 : ∀ (s : ↥S), IsNoetherianRing.{u} (Localization.Away (↑s : R))
⊢ IsNoetherianRing R
have 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)
Tactic: apply monotone_stabilizes_iff_noetherian.mp
-- 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 : ∀ (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)
have h : (suitableN (↑s : R)).Nonempty
Tactic: apply Nat.sInf_mem
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
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)
⊢ ∃ (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)
have hSuit : ∀ (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
-- 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 : ∀ (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
⊢ ∃ (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)
have 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)
Tactic: use N
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Noetherian (hypothesis)
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
⊢ ∀ (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)
have hN₁ : ∀ (s : ↥S), minN (↑s : R) ≤ N
Tactic: have hN : ∀ s : S, minN s ≤ N := fun s => Finset.le_sup s.prop
-- 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
⊢ Eq (α := Submodule R R) ((I : (a : ℕ) → Submodule R R) N : Submodule R R)
    ((I : (a : ℕ) → Submodule R R) n : Submodule R R)
have 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)))
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']
-- 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
⊢ 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)))
have 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)))
Tactic: apply iInf_congr