-- Lean 4 proof step from Mathlib.RingTheory.Ideal.KrullsHeightTheorem (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsNoetherianRing R
S : Type u_2
inst_2 : CommRing S
inst_3 : Algebra R S
inst_4 : IsNoetherianRing S
inst_5 : Algebra.HasGoingDown R S
p : Ideal R
inst_6 : p.IsPrime
P : Ideal S
inst_7 : P.IsPrime
inst_8 : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp :
  RelSeries.last (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
      lp =
    { asIdeal := p, isPrime := ⋯ }
hlenp :
  (↑(lp.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞) =
    p.height
⊢ p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P) ≤
    P.height
have obtain : ∀ (lq : LTSeries (PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))))
  (hlq :
    RelSeries.last (r :=
        {x :
          PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
          match (motive :=
            PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
              Prop)
            x with
          | (a, b) => a < b})
        lq =
      {
        asIdeal :=
          map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
            (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P,
        isPrime := sorry })
  (hlenq :
    (↑(lq.length (r :=
            {x :
              PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) |
              match (motive :=
                PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) ×
                    PrimeSpectrum (HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p)) →
                  Prop)
                x with
              | (a, b) => a < b})) :
        ℕ∞) =
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P)),
  p.height +
      height (R := HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
        (map (F := S →+* HasQuotient.Quotient S (B := Ideal S) (map (F := R →+* S) (algebraMap R S) p))
          (Quotient.mk (map (F := R →+* S) (algebraMap R S) p)) P) ≤
    P.height
Tactic: obtain ⟨lq, hlq, hlenq⟩ :=
    (P.map (Quotient.mk (p.map (algebraMap R S)))).exists_ltSeries_length_eq_height