-- Module: Mathlib.RingTheory.Ideal.GoingDown
Goal:
R : Type u_1
S : Type u_2
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.HasGoingDown R S
l :
  RelSeries (α := PrimeSpectrum R)
    {x : PrimeSpectrum R × PrimeSpectrum R |
      match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
      | (a, b) => a < b}
q : PrimeSpectrum R
lt :
  Membership.mem (γ := SetRel (PrimeSpectrum R) (PrimeSpectrum R))
    {x : PrimeSpectrum R × PrimeSpectrum R |
      match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
      | (a, b) => a < b}
    (q,
      l.head (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b}))
ih :
  ∀ (P : Ideal S) [inst_5 : P.IsPrime]
    [lo :
      P.LiesOver
        l.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b}).asIdeal],
    ∃ (L : LTSeries (PrimeSpectrum S)),
      L.length (r :=
            {x : PrimeSpectrum S × PrimeSpectrum S |
              match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
              | (a, b) => a < b}) =
          l.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b}) ∧
        RelSeries.last (r :=
              {x : PrimeSpectrum S × PrimeSpectrum S |
                match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
                | (a, b) => a < b})
              L =
            { asIdeal := P, 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})
                L) =
            l.toList (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
P : Ideal S
inst_4 : P.IsPrime
lo : P.LiesOver l.last (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2}).asIdeal
L : LTSeries (PrimeSpectrum S)
len :
  L.length (r :=
      {x : PrimeSpectrum S × PrimeSpectrum S |
        match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
        | (a, b) => a < b}) =
    l.length (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
last :
  RelSeries.last (r :=
      {x : PrimeSpectrum S × PrimeSpectrum S |
        match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
        | (a, b) => a < b})
      L =
    { asIdeal := P, isPrime := ⋯ }
spec :
  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})
        L) =
    l.toList (r :=
      {x : PrimeSpectrum R × PrimeSpectrum R |
        match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
        | (a, b) => a < b})
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
    l.head (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b}).asIdeal
Q : Ideal S
Qlt :
  Q <
    (RelSeries.head (r :=
        {x : PrimeSpectrum S × PrimeSpectrum S |
          match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
          | (a, b) => a < b})
        L).asIdeal
hQ : Q.IsPrime
Qlo : Q.LiesOver q.asIdeal
h :
  L.length (r := {x : PrimeSpectrum S × PrimeSpectrum S | x.1 < x.2}) =
      l.length (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2}) ∧
    RelSeries.last (r := {x : PrimeSpectrum S × PrimeSpectrum S | x.1 < x.2}) L = { asIdeal := P, isPrime := ⋯ } ∧
      List.map (PrimeSpectrum.comap (algebraMap R S))
          ((RelSeries.cons (r := {x : PrimeSpectrum S × PrimeSpectrum S | x.1 < x.2}) L
                { asIdeal := Q, isPrime := hQ : PrimeSpectrum S } Qlt).toList
            (r := {x : PrimeSpectrum S × PrimeSpectrum S | x.1 < x.2})) =
        (l.cons (r := {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2}) q lt).toList (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R | x.1 < x.2})
⊢ (RelSeries.cons (r :=
            {x : PrimeSpectrum S × PrimeSpectrum S |
              match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
              | (a, b) => a < b})
            L { asIdeal := Q, isPrime := hQ : PrimeSpectrum S } Qlt).length
        (r :=
        {x : PrimeSpectrum S × PrimeSpectrum S |
          match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
          | (a, b) => a < b}) =
      (l.cons (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            q lt).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 S × PrimeSpectrum S |
                match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
                | (a, b) => a < b})
              L { asIdeal := Q, isPrime := hQ : PrimeSpectrum S } Qlt).last
          (r :=
          {x : PrimeSpectrum S × PrimeSpectrum S |
            match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
            | (a, b) => a < b}) =
        { asIdeal := P, isPrime := ⋯ } ∧
      List.map (PrimeSpectrum.comap (algebraMap R S))
          ((RelSeries.cons (r :=
                {x : PrimeSpectrum S × PrimeSpectrum S |
                  match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
                  | (a, b) => a < b})
                L { asIdeal := Q, isPrime := hQ : PrimeSpectrum S } Qlt).toList
            (r :=
            {x : PrimeSpectrum S × PrimeSpectrum S |
              match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
              | (a, b) => a < b})) =
        (l.cons (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              q lt).toList
          (r :=
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b})

Tactic:
simp only [RelSeries.cons_length, add_left_inj, RelSeries.last_cons]

Premises used: RelSeries.last_cons, add_left_inj, RelSeries.cons_length