-- Lean 4 proof step from Mathlib.RingTheory.Length (goal)
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)
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})) :
      ℕ∞)
have a : ∀
  (this :
    Fin
        (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})) ≃
      Fin
        (t'.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: have := (s.jordan_holder t' (h₁.trans ht₁.symm) (h₂.trans ht₂.symm)).choose