-- Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem
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
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 := ⋯ }
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)
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (F := R →+* S) (algebraMap R S) p))) ⋯
this :
  (RelSeries.head (r :=
          {x : PrimeSpectrum S × PrimeSpectrum S |
            match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
            | (a, b) => a < b})
          l').asIdeal.LiesOver
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        lp).asIdeal
obtain :
  ∀ (lp' : LTSeries (PrimeSpectrum S))
    (hlp'len :
      lp'.length (r :=
          {x : PrimeSpectrum S × PrimeSpectrum S |
            match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
            | (a, b) => a < b}) =
        lp.length (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}))
    (hlp' :
      RelSeries.last (r :=
          {x : PrimeSpectrum S × PrimeSpectrum S |
            match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
            | (a, b) => a < b})
          lp' =
        {
          asIdeal :=
            (RelSeries.head (r :=
                {x : PrimeSpectrum S × PrimeSpectrum S |
                  match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
                  | (a, b) => a < b})
                l').asIdeal,
          isPrime := ⋯ }),
    List.map (PrimeSpectrum.comap (algebraMap R S))
          (RelSeries.toList (r :=
            {x : PrimeSpectrum S × PrimeSpectrum S |
              match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
              | (a, b) => a < b})
            lp') =
        RelSeries.toList (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})
          lp →
      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
⊢ 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 ⟨lp', hlp'len, hlp', _⟩ := exists_ltSeries_of_hasGoingDown lp l'.head.asIdeal

Premises used: Ideal.exists_ltSeries_of_hasGoingDown, RelSeries.head, PrimeSpectrum.asIdeal