-- 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 : LTSeries (PrimeSpectrum R)
P : Ideal S
inst_4 : P.IsPrime
lo :
  P.LiesOver
    (RelSeries.last (r :=
        {x : PrimeSpectrum R × PrimeSpectrum R |
          match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
          | (a, b) => a < b})
        l).asIdeal
singleton :
  ∀ (q : PrimeSpectrum R) (P : Ideal S) [inst_5 : P.IsPrime]
    [lo :
      P.LiesOver
        (RelSeries.last (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            (RelSeries.singleton
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b}
              q)).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}) =
          RelSeries.length (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            (RelSeries.singleton
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b}
              q) ∧
        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) =
            RelSeries.toList (r :=
              {x : PrimeSpectrum R × PrimeSpectrum R |
                match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                | (a, b) => a < b})
              (RelSeries.singleton
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b}
                q)
cons :
  ∀
    (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_5 : P.IsPrime]
    [lo :
      P.LiesOver
        (l.cons (r :=
                {x : PrimeSpectrum R × PrimeSpectrum R |
                  match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
                  | (a, b) => a < b})
                q lt).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.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.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.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})
⊢ ∃ (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) =
          RelSeries.toList (r :=
            {x : PrimeSpectrum R × PrimeSpectrum R |
              match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
              | (a, b) => a < b})
            l

Tactic:
induction l using RelSeries.inductionOn generalizing P with
  | singleton q =>
    use RelSeries.singleton _ ⟨P, inferInstance⟩
    simp only [RelSeries.singleton_length, RelSeries.last_singleton, RelSeries.toList_singleton,
      List.map_cons, List.map_nil, List.cons.injEq, and_true, true_and]
    ext : 1
    simpa using lo.over.symm
  | cons l q lt ih =>
    simp only [RelSeries.last_cons] at lo
    obtain ⟨L, len, last, spec⟩ := ih P
    have : L.head.asIdeal.LiesOver l.head.asIdeal := by
      constructor
      rw [← L.toList_getElem_zero_eq_head, ← l.toList_getElem_zero_eq_head, Ideal.under_def]
      have : l.toList[0] = (PrimeSpectrum.comap (algebraMap R S)) L.toList[0] := by
        rw [List.getElem_map_rev (PrimeSpectrum.comap (algebraMap R S)),
          List.getElem_of_eq spec.symm _]
      rwa [PrimeSpectrum.ext_iff] at this
    obtain ⟨Q, Qlt, hQ, Qlo⟩ := Ideal.exists_ideal_lt_liesOver_of_lt L.head.asIdeal lt
    use L.cons ⟨Q, hQ⟩ Qlt
    simp only [RelSeries.cons_length, add_left_inj, RelSeries.last_cons]
    exact ⟨len, last, by simpa [spec] using PrimeSpectrum.ext_iff.mpr Qlo.over.symm⟩

Premises used: RelSeries.toList_singleton, and_true, List.map_cons, RelSeries.last_cons, add_left_inj, List.cons.injEq, RelSeries.cons_length, RelSeries.singleton_length, Ideal.LiesOver.over, Singleton.singleton, Eq.symm, RelSeries.singleton, RelSeries.last_singleton, true_and, List.map_nil