-- 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
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
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)
⊢ 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

Tactic:
obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp (hn.le (Ideal.mem_sup_left hx))

Premises used: Ideal.mem_sup_left, Eq.le, Iff.mp, Submodule.mem_sup, rfl