awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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))ᵒᵈ)
⊢ Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime q)) ⊥ ⊤

Tactic:
bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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))ᵒᵈ)
⊢ Ne.{u_1 + 1} (α := Ideal (Localization.AtPrime q)) ⊥ ⊤

Tactic:
exact bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 :
  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)
⊢ 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:
rw [smul_eq_mul, ← pow_succ',
    ← (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)).map_rel_iff]

Premises used: Localization.AtPrime, IsLocalization.orderEmbedding, RelEmbedding.map_rel_iff, Ideal.primeCompl, smul_eq_mul, pow_succ'
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)

Tactic:
Submodule.le_of_le_smul_of_le_jacobson_bot (I := I) (IsNoetherian.noetherian _) ?_ ?_

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot, Set.Mem, IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 ⊥
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)
⊢ 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:
refine Submodule.le_of_le_smul_of_le_jacobson_bot (I := I) (IsNoetherian.noetherian _) ?_ ?_

Premises used: Submodule.le_of_le_smul_of_le_jacobson_bot, IsNoetherian.noetherian
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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
hIN₁ : Ne.{u_1 + 1} (α := Ideal R) ⊥ ⊤
⊢ I ≤ jacobson ⊥

Tactic:
rw [IsLocalRing.jacobson_eq_maximalIdeal]

Premises used: IsLocalRing.jacobson_eq_maximalIdeal
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 ≤ IsLocalRing.maximalIdeal R

Tactic:
hp.le

Premises used: Ideal.IsMinimalPrime.le
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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))ᵒᵈ)
⊢ Ne.{u_1 + 1} (α := Ideal R) ⊥ ⊤

Tactic:
bot_ne_top

Premises used: bot_ne_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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 ≤ IsLocalRing.maximalIdeal R

Tactic:
exacts [hp.le, bot_ne_top]

Premises used: Ideal.IsMinimalPrime.le, bot_ne_top
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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))ᵒᵈ)
⊢ 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))
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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))
⊢ 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

Premises used: OrderHom.coe_mk, Ideal.Quotient.mk_surjective, Ideal.comap_map_of_surjective, RingHom.ker_eq_comap_bot, Ideal.mk_ker
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)

Tactic:
Submodule.add_mem_sup hy ?_

Premises used: Set.Mem, setOf, Submodule.add_mem_sup
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)
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)
⊢ 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:
refine Submodule.add_mem_sup hy ?_

Premises used: Submodule.add_mem_sup
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)
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)
⊢ 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:
obtain ⟨z, rfl⟩ := (Submodule.IsPrincipal.mem_iff_eq_smul_generator I).mp hz

Premises used: Submodule.IsPrincipal.mem_iff_eq_smul_generator, Iff.mp, rfl
-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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)
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
⊢ 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:
rw [smul_eq_mul, smul_eq_mul, mul_comm]

Premises used: mul_comm, smul_eq_mul