-- Lean 4 proof step from Mathlib.RingTheory.KrullDimension.NonZeroDivisors (goal)
Goal:
R : Type u_1
inst : CommRing R
r : R
hr : Membership.mem (γ := Submonoid R) R⁰ r
hr' : ¬Eq (α := Ideal R) (Ideal.span {r}) ⊤
this_1 : Nonempty.{u_1 + 1} (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
this_2 : Nontrivial.{u_1} (HasQuotient.Quotient R (B := Ideal R) (Ideal.span {r}))
this : Nontrivial R
l : LTSeries (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1)
p : Ideal R
hp : Membership.mem (γ := Set (Ideal R)) (Ideal.minimalPrimes ⊥) p
hp'_1 :
  p ≤
    (↑(RelSeries.head (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})
            l) :
        PrimeSpectrum R).asIdeal
p' : PrimeSpectrum R := { asIdeal := p, isPrime := ⋯ }
hp' :
  p' <
    (↑(RelSeries.head (r :=
          {x :
            (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
            match (motive :=
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                Prop)
              x with
            | (a, b) => a < b})
          l) :
      PrimeSpectrum R)
⊢ HAdd.hAdd (α := ℕ∞)
      (↑(l.length (r :=
            {x :
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
              match (motive :=
                (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                    (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                  Prop)
                x with
              | (a, b) => a < b})) :
        ℕ∞)
      1 ≤
    ⨆ (p : LTSeries (PrimeSpectrum R)),
      (↑(p.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
have neg : HAdd.hAdd (α := ℕ∞)
    (↑(l.length (r :=
          {x :
            (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) |
            match (motive :=
              (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) ×
                  (↑(PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) : Type u_1) →
                Prop)
              x with
            | (a, b) => a < b})) :
      ℕ∞)
    1 ≤
  (↑(RelSeries.length (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        (RelSeries.cons (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          (l.map
            (Subtype.val (p := fun (x : PrimeSpectrum R) ↦
              Membership.mem (γ := Set (PrimeSpectrum R)) (PrimeSpectrum.zeroLocus (↑(Ideal.span {r}) : Set R)) x))
            sorry)
          p' hp')) :
    ℕ∞)
Tactic: refine le_trans ?_ (le_iSup _ ((l.map Subtype.val (fun _ _ ↦ id)).cons p' hp'))