-- Module: Mathlib.RingTheory.Length
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
h₁ :
  RelSeries.head (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊥
h₂ :
  RelSeries.last (r :=
      {x : Submodule R M × Submodule R M |
        match (motive := Submodule R M × Submodule R M → Prop) x with
        | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})
      s =
    ⊤
H : IsFiniteLength R M
this_1 : IsNoetherian R M
this : IsArtinian R M
t : LTSeries (Submodule R M)
a :
  ∀
    (t' :
      RelSeries (α := Submodule R M)
        {x : Submodule R M × Submodule R M |
          match (motive := Submodule R M × Submodule R M → Prop) x with
          | (a, b) => a ⋖ b})
    (i :
      Fin
          (t.length (r :=
              {x : Submodule R M × Submodule R M |
                match (motive := Submodule R M × Submodule R M → Prop) x with
                | (a, b) => a < b}) +
            1) ↪
        Fin
          (t'.length (r :=
              {x : Submodule R M × Submodule R M |
                match (motive := Submodule R M × Submodule R M → Prop) x with
                | (a, b) => a ⋖ b}) +
            1))
    (hi :
      t'.toFun (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (a, b) => a ⋖ b}) ∘
          (⇑i : (a : Fin (t.length + 1)) → Fin (t'.length + 1)) =
        t.toFun (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (a, b) => a < b}))
    (ht₁ :
      t'.head (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (a, b) => a ⋖ b}) =
        ⊥)
    (ht₂ :
      t'.last (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (a, b) => a ⋖ b}) =
        ⊤),
    LE.le (α := ℕ∞)
      (↑(t.length (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (a, b) => a < b})) :
        ℕ∞)
      (↑(s.length (r :=
            {x : Submodule R M × Submodule R M |
              match (motive := Submodule R M × Submodule R M → Prop) x with
              | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})) :
        ℕ∞)
⊢ LE.le (α := ℕ∞)
    (↑(t.length (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (a, b) => a < b})) :
      ℕ∞)
    (↑(s.length (r :=
          {x : Submodule R M × Submodule R M |
            match (motive := Submodule R M × Submodule R M → Prop) x with
            | (x, y) => @JordanHolderLattice.IsMaximal _ ConditionallyCompleteLattice.toLattice _ x y})) :
      ℕ∞)

Tactic:
obtain ⟨t', i, hi, ht₁, ht₂⟩ := t.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot

Premises used: LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot