-- Lean 4 proof step from Mathlib.RingTheory.FiniteLength (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
s : CompositionSeries (Submodule R M)
s_head :
  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 =
    ⊥
s_last :
  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 =
    ⊤
i :
  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}))
ih :
  IsFiniteLength.{u_1, u_2} R
    ↥(s.toFun (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})
        i.castSucc)
cov : Membership.mem (γ := SetRel (Submodule R M) (Submodule R M))
  {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.toFun (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})
      i.castSucc,
    s.toFun (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})
      i.succ) :=
  ⋯
this :
  IsSimpleModule.{u_1, u_2} R
    (↥(s.toFun (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})
          i.succ) ⧸
      Submodule.comap
        (s.toFun (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})
            i.succ).subtype
        (s.toFun (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})
          i.castSucc))
⊢ IsFiniteLength.{u_1, u_2} R
    ↥(s.toFun (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})
        i.succ)
have succ : ∀
  (this :
    ↥(Submodule.comap
          (s.toFun (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})
              i.succ).subtype
          (s.toFun (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})
            i.castSucc)) ≃ₗ[R]
      ↥(Submodule.map
          (s.toFun (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})
              i.succ).subtype
          (Submodule.comap
            (s.toFun (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})
                i.succ).subtype
            (s.toFun (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})
              i.castSucc)))),
  IsFiniteLength.{u_1, u_2} R
    ↥(s.toFun (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})
        i.succ)
Tactic: have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective
        _ (Submodule.injective_subtype _)