-- 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
q : 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})
        (RelSeries.singleton
          {x : PrimeSpectrum R × PrimeSpectrum R |
            match (motive := PrimeSpectrum R × PrimeSpectrum R → Prop) x with
            | (a, b) => a < b}
          q)).asIdeal
h : PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S } = q
⊢ RelSeries.length (r :=
        {x : PrimeSpectrum S × PrimeSpectrum S |
          match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
          | (a, b) => a < b})
        (RelSeries.singleton
          {x : PrimeSpectrum S × PrimeSpectrum S |
            match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
            | (a, b) => a < b}
          { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S }) =
      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})
          (RelSeries.singleton
            {x : PrimeSpectrum S × PrimeSpectrum S |
              match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
              | (a, b) => a < b}
            { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S }) =
        { 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})
            (RelSeries.singleton
              {x : PrimeSpectrum S × PrimeSpectrum S |
                match (motive := PrimeSpectrum S × PrimeSpectrum S → Prop) x with
                | (a, b) => a < b}
              { asIdeal := P, isPrime := ⋯ : PrimeSpectrum S })) =
        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)

Tactic:
simp only [RelSeries.singleton_length, RelSeries.last_singleton, RelSeries.toList_singleton,
      List.map_cons, List.map_nil, List.cons.injEq, and_true, true_and]

Premises used: RelSeries.toList_singleton, and_true, List.map_cons, List.cons.injEq, RelSeries.singleton_length, RelSeries.last_singleton, true_and, List.map_nil