-- Mathlib/RingTheory/FiniteLength.lean
theorem isFiniteLength_of_exists_compositionSeries
    (h : ∃ s : CompositionSeries (Submodule R M), s.head = ⊥ ∧ s.last = ⊤) :
    IsFiniteLength R M :=
  Submodule.topEquiv.isFiniteLength <| by
    obtain ⟨s, s_head, s_last⟩ := h
    rw [← s_last]
    suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)
    intro i
    induction' i using Fin.induction with i ih
    · change IsFiniteLength R s.head; rw [s_head]; exact .of_subsingleton
    let cov := s.step i
    have := (covBy_iff_quot_is_simple cov.le).mp cov
    have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective
      _ (Submodule.injective_subtype _)
    rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this
    exact .of_simple_quotient (this.symm.isFiniteLength ih)

Proof state:
case intro.intro.succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : JordanHolderLattice.IsMaximal (s.toFun i.castSucc) (s.toFun i.succ) := s.step i
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Tactic:
have := (covBy_iff_quot_is_simple cov.le).mp cov

Result:
case intro.intro.succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : JordanHolderLattice.IsMaximal (s.toFun i.castSucc) (s.toFun i.succ) := s.step i
this : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Proof state:
case intro.intro.succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : JordanHolderLattice.IsMaximal (s.toFun i.castSucc) (s.toFun i.succ) := s.step i
this : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Tactic:
have := ((s i.castSucc).comap (s i.succ).subtype).equivMapOfInjective
  _ (Submodule.injective_subtype _)

Result:
case intro.intro.succ
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
i : Fin s.length
ih : IsFiniteLength R ↥(s.toFun i.castSucc)
cov : JordanHolderLattice.IsMaximal (s.toFun i.castSucc) (s.toFun i.succ) := s.step i
this✝ : IsSimpleModule R (↥(s.toFun i.succ) ⧸ Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc))
this :
  ↥(Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R]
    ↥(Submodule.map (s.toFun i.succ).subtype (Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)))
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Proof state:
case intro.intro.zero
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : CompositionSeries (Submodule R M)
s_head : RelSeries.head s = ⊥
s_last : RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥⊥

Tactic:
exact .of_subsingleton

Result:
no goals