awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z ∈ I
hx :
  Membership.mem (γ := Submodule R R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    (y + z)
⊢ z ∈
    HSMul.hSMul (β := Submodule R R) I
      ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q))
            (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
        Ideal R)
have hIN : ∀ (z : R) (hz : z • Submodule.IsPrincipal.generator I ∈ I)
  (hx :
    Membership.mem (γ := Submodule R R)
      ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q))
            (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
        Ideal R)
      (y + z • Submodule.IsPrincipal.generator I)),
  z • Submodule.IsPrincipal.generator I ∈
    HSMul.hSMul (β := Submodule R R) I
      ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q))
            (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
        Ideal R)
Tactic: obtain ⟨z, rfl⟩ := (Submodule.IsPrincipal.mem_iff_eq_smul_generator I).mp hz
Cleared hypotheses: z, hz, hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  Membership.mem (γ := Submodule R R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    (y + z • Submodule.IsPrincipal.generator I)
⊢ z • Submodule.IsPrincipal.generator I ∈
    HSMul.hSMul (β := Submodule R R) I
      ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q))
            (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
        Ideal R)
have hIN : z * Submodule.IsPrincipal.generator I ∈
  HMul.hMul (α := Ideal R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    I
Tactic: rw [smul_eq_mul, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  Membership.mem (γ := Submodule R R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    (y + z • Submodule.IsPrincipal.generator I)
⊢ z * Submodule.IsPrincipal.generator I ∈
    HMul.hMul (α := Ideal R)
      ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q))
            (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
        Ideal R)
      I
have hIN : Membership.mem (γ := Ideal R)
  ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
        (a : Ideal (Localization.AtPrime q)) → Ideal R)
      (HPow.hPow (α := Ideal (Localization.AtPrime q))
        (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
    Ideal R)
  z
Tactic: refine Ideal.mul_mem_mul ?_ (Submodule.IsPrincipal.generator_mem _)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  Membership.mem (γ := Submodule R R)
    (under R
      (HPow.hPow (α := Ideal (Localization.AtPrime q))
        (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n))
    (y + z * Submodule.IsPrincipal.generator I)
⊢ Membership.mem (γ := Ideal R)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q))
          (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n) :
      Ideal R)
    z
have hIN : ∀
  (hx :
    HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
        ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
        ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
      HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n),
  IsUnit (M := Localization.AtPrime q)
    ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
Tactic: rwa [Ideal.mem_comap, f.map_add, f.map_mul, Ideal.add_mem_iff_right _
      (Ideal.pow_le_pow_right n.le_succ hy), mul_comm, Ideal.unit_mul_mem_iff_mem] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
⊢ IsUnit (M := Localization.AtPrime q)
    ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
have hIN : (Classical.indefiniteDescription (fun (x : R) ↦ I = R ∙ x) sorry).1 ∈ q.primeCompl
Tactic: refine IsLocalization.map_units (M := q.primeCompl) _ ⟨_, ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
⊢ (Classical.indefiniteDescription (fun (x : R) ↦ I = R ∙ x) ⋯).1 ∈ q.primeCompl
have hIN : Submodule.IsPrincipal.generator I ∉ (↑q : Set R)
Tactic: change Submodule.IsPrincipal.generator I ∉ (↑q : Set R)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
inst_2 : IsLocalRing R
I : Ideal R
inst_3 : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing.{u_1} (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
  {
    toFun := fun (n : ℕ) ↦
      map (F := R →+* R ⧸ I) (Quotient.mk I) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n)),
    monotone' := ⋯ }
n : ℕ
hn :
  comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n) ⊔ I =
    comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ) ⊔ I
y : R
hy : Membership.mem (γ := Submodule R R) (comap f (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n.succ)) y
z : R
hz : z • Submodule.IsPrincipal.generator I ∈ I
hx :
  HMul.hMul (α := Localization.AtPrime q) (β := Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) (Submodule.IsPrincipal.generator I) : Localization.AtPrime q)
      ((f : (a : R) → Localization.AtPrime q) z : Localization.AtPrime q) ∈
    HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) n
⊢ Submodule.IsPrincipal.generator I ∉ (↑q : Set R)
have hIN : ¬I ≤ q
Tactic: rw [← Set.singleton_subset_iff, ← Ideal.span_le, Ideal.span_singleton_generator]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
⊢ p.height ≤ 1
have this : p.IsPrime
Tactic: have := hp.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ p.height ≤ 1
have refine_2 : ∀ (this : height.{u_1} (R := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ≤ 1),
  p.height ≤ 1
Tactic: have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
refine_2 :
  ∀ (this : height.{u_1} (R := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ≤ 1),
    p.height ≤ 1
⊢ p.height ≤ 1
have refine_1 : Membership.mem (γ := Set (Ideal (Localization.AtPrime p))) (Ideal.minimalPrimes (map f I))
  (IsLocalRing.maximalIdeal (Localization.AtPrime p))
Tactic: have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this_1 : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
this : height.{u_1} (R := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ≤ 1
⊢ p.height ≤ 1
have refine_2 : ∀ (this : height (under R (B := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p))) ≤ 1),
  p.height ≤ 1
Tactic: rwa [← IsLocalization.height_under p.primeCompl,
      Localization.AtPrime.under_maximalIdeal] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this_1 : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
this : height.{u_1} (R := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ≤ 1
refine_2 :
  ∀ (this : height (under R (B := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p))) ≤ 1),
    p.height ≤ 1
⊢ p.height ≤ 1
have refine_2₁ : ∀ (this : p.height ≤ 1), p.height ≤ 1
Tactic: rwa [← IsLocalization.height_under p.primeCompl,
      Localization.AtPrime.under_maximalIdeal] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
⊢ Membership.mem (γ := Set (Ideal (Localization.AtPrime p))) (Ideal.minimalPrimes (map f I))
    (IsLocalRing.maximalIdeal (Localization.AtPrime p))
have refine_1 : Membership.mem (γ := Set (Ideal (Localization.AtPrime p))) (under R ⁻¹' I.minimalPrimes)
  (IsLocalRing.maximalIdeal (Localization.AtPrime p))
Tactic: rwa [IsLocalization.minimalPrimes_map p.primeCompl (Localization.AtPrime p) I,
      Set.mem_preimage, Localization.AtPrime.under_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
I : Ideal R
inst_2 : Submodule.IsPrincipal I
p : Ideal R
hp : p ∈ I.minimalPrimes
this : p.IsPrime
f : R →+* Localization.AtPrime p := algebraMap R (Localization.AtPrime p)
refine_1 :
  Membership.mem (γ := Set (Ideal (Localization.AtPrime p))) (under R ⁻¹' I.minimalPrimes)
    (IsLocalRing.maximalIdeal (Localization.AtPrime p))
⊢ Membership.mem (γ := Set (Ideal (Localization.AtPrime p))) (Ideal.minimalPrimes (map f I))
    (IsLocalRing.maximalIdeal (Localization.AtPrime p))
have refine_1₁ : under R (B := Localization.AtPrime p) (IsLocalRing.maximalIdeal (Localization.AtPrime p)) ∈ I.minimalPrimes
Tactic: rwa [IsLocalization.minimalPrimes_map p.primeCompl (Localization.AtPrime p) I,
      Set.mem_preimage, Localization.AtPrime.under_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
⊢ height (R := R) (span {x}) ≤ 1
have obtain : ∀ (p : Ideal R) (hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) p),
  height (R := R) (span {x}) ≤ 1
Tactic: obtain ⟨p, hp⟩ := (span {x}).nonempty_minimalPrimes (by simpa)
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span {x})) p
⊢ height (R := R) (span {x}) ≤ 1
have refine : p.height ≤ 1
Tactic: refine le_trans (height_mono hp.1.2) ?_
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
Tactic: have hf : Function.Surjective f := Quotient.mk_surjective
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have hI'q : span t ≤ q
Tactic: have hI'q : span t ≤ q := span_le.mpr htq
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have hI'p : span t ≤ p
Tactic: have hI'p : span t ≤ p := hI'q.trans hqp.le
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have this : p.IsPrime
Tactic: have := hp.isPrime
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
q p : Ideal R
inst_2 : q.IsPrime
hqp : q < p
x : R
s : Set R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span (insert x s))) p
t : Set R
htq : t ⊆ (↑q : Set R)
hsp : s ⊆ (↑(radical (span (insert x t))) : Set R)
f : R →+* HasQuotient.Quotient R (B := Ideal R) (span t) := Quotient.mk (span t)
hf : Function.Surjective (α := R) (β := HasQuotient.Quotient R (B := Ideal R) (span t)) (⇑f : (a : R) → R ⧸ span t)
hI'q : span t ≤ q
hI'p : span t ≤ p
this : p.IsPrime
⊢ Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes (span t)) q
have this₁ : IsPrime (α := HasQuotient.Quotient R (B := Ideal R) (span t)) (map f p)
Tactic: have : (p.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])