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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
⊢ IsNilpotent (R := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q)
have refine : HPow.hPow (α := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n =
  0
Tactic: refine ⟨n, ?_⟩
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
⊢ HPow.hPow (α := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n =
    0
have hIN : HPow.hPow (α := Ideal (Localization.AtPrime q))
    (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n ≤
  HSMul.hSMul (α := Ideal (Localization.AtPrime q)) (map f q)
    (HPow.hPow (α := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n)
Tactic: apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (q.map f) _ (IsNoetherian.noetherian _)
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
hIN :
  HPow.hPow (α := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n ≤
    HSMul.hSMul (α := Ideal (Localization.AtPrime q)) (map f q)
      (HPow.hPow (α := Ideal (Localization.AtPrime q))
        (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n)
⊢ HPow.hPow (α := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n =
    0
have hIjac : LE.le (α := Ideal (Localization.AtPrime q)) (map f q) (jacobson ⊥)
Tactic: apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (q.map f) _ (IsNoetherian.noetherian _)
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
⊢ LE.le (α := Ideal (Localization.AtPrime q)) (map f q) (jacobson ⊥)
have hIjac : Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime q)) ⊥ ⊤
Tactic: rw [IsLocalRing.jacobson_eq_maximalIdeal, Localization.AtPrime.map_eq_maximalIdeal]
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
⊢ HPow.hPow (α := Ideal (Localization.AtPrime q))
      (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n ≤
    HSMul.hSMul (α := Ideal (Localization.AtPrime q)) (map f q)
      (HPow.hPow (α := Ideal (Localization.AtPrime q))
        (map (F := R →+* Localization.AtPrime q) (algebraMap R (Localization.AtPrime q)) q) n)
have hIN : LE.le (α := 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)
  ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
        (a : Ideal (Localization.AtPrime q)) → Ideal R)
      (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) (n + 1)) :
    Ideal R)
Tactic: rw [smul_eq_mul, ← pow_succ',
    ← (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)).map_rel_iff]
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
⊢ LE.le (α := 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)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) (n + 1)) :
      Ideal R)
have hIN : I ≤ jacobson ⊥
Tactic: refine Submodule.le_of_le_smul_of_le_jacobson_bot (I := I) (IsNoetherian.noetherian _) ?_ ?_
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
hIN : I ≤ jacobson ⊥
⊢ LE.le (α := 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)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) (n + 1)) :
      Ideal R)
have hIN₁ : LE.le (α := 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)
  ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
          (a : Ideal (Localization.AtPrime q)) → Ideal R)
        (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) (n + 1)) ⊔
      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) :
    Submodule R R)
Tactic: refine Submodule.le_of_le_smul_of_le_jacobson_bot (I := I) (IsNoetherian.noetherian _) ?_ ?_
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
⊢ I ≤ jacobson ⊥
have hIN : I ≤ IsLocalRing.maximalIdeal R
Tactic: rw [IsLocalRing.jacobson_eq_maximalIdeal]
-- 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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
hIN : I ≤ IsLocalRing.maximalIdeal R
⊢ I ≤ jacobson ⊥
have hIN₁ : Ne.{u_1 + 1} (α := Ideal R) ⊥ ⊤
Tactic: rw [IsLocalRing.jacobson_eq_maximalIdeal]
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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 :
  ∀ (m : ℕ),
    n ≤ m →
      Eq (α := (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
        ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) m : (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ)
⊢ LE.le (α := 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)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) (n + 1)) ⊔
        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) :
      Submodule R R)
have hn₁ : Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n))
  (comap (F := R →+* R ⧸ I) (Quotient.mk I) ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n.succ))
Tactic: replace hn := congr(Ideal.comap (Ideal.Quotient.mk I) $(hn _ n.le_succ))
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (hypothesis)
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 :
  Eq (α := Ideal R) (comap (F := R →+* R ⧸ I) (Quotient.mk I) ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n))
    (comap (F := R →+* R ⧸ I) (Quotient.mk I) ((qs : (a : ℕ) → (Submodule (R ⧸ I) (R ⧸ I))ᵒᵈ) n.succ))
⊢ LE.le (α := 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)
    ((IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q) :
            (a : Ideal (Localization.AtPrime q)) → Ideal R)
          (HPow.hPow (α := Ideal (Localization.AtPrime q)) (map f q) (n + 1)) ⊔
        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) :
      Submodule R R)
have 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
Tactic: simp only [qs, OrderHom.coe_mk, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker,
      Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective] at hn
Cleared hypotheses: hn
-- 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
x : R
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)
    x
⊢ 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 q) (n + 1)) ⊔
        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) :
      Submodule R R)
    x
have hIN : ∀ (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)),
  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 q) (n + 1)) ⊔
        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) :
      Submodule R R)
    (y + z)
Tactic: obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp (hn.le (Ideal.mem_sup_left hx))
Cleared hypotheses: x, 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 ∈ 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)
⊢ 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 q) (n + 1)) ⊔
        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) :
      Submodule R R)
    (y + z)
have hIN : 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)
Tactic: refine Submodule.add_mem_sup hy ?_