-- 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
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)

Tactic:
rw [Submodule.map_comap_subtype, inf_of_le_right cov.le] at this

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] ↥(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 ↥(s.toFun 0)

Tactic:
change IsFiniteLength R s.head

Result:
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 ↥(RelSeries.head s)

Proof state:
case intro.intro
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 + 1)
⊢ IsFiniteLength R ↥(s.toFun i)

Tactic:
induction' i using Fin.induction with i ih

Result:
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 ↥(s.toFun 0)

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)
⊢ 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))
this : ↥(Submodule.comap (s.toFun i.succ).subtype (s.toFun i.castSucc)) ≃ₗ[R] ↥(s.toFun i.castSucc)
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Tactic:
exact .of_simple_quotient (this.symm.isFiniteLength ih)

Result:
no goals

Proof state:
case intro.intro
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 + 1)), IsFiniteLength R ↥(s.toFun i)

Tactic:
intro i

Result:
case intro.intro
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 + 1)
⊢ IsFiniteLength R ↥(s.toFun i)

Proof state:
case intro.intro
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 ↥(RelSeries.last s)

Tactic:
suffices ∀ i, IsFiniteLength R (s i) from this (Fin.last _)

Result:
case intro.intro
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 + 1)), IsFiniteLength R ↥(s.toFun i)

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)
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Tactic:
let cov := s.step i

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
⊢ IsFiniteLength R ↥(s.toFun i.succ)

Proof state:
R : Type u_1
inst✝² : Ring R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤
⊢ IsFiniteLength R ↥⊤

Tactic:
obtain ⟨s, s_head, s_last⟩ := h

Result:
case intro.intro
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 ↥⊤

Proof state:
case intro.intro
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:
rw [← s_last]

Result:
case intro.intro
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 ↥(RelSeries.last s)

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 ↥(RelSeries.head s)

Tactic:
rw [s_head]

Result:
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 ↥⊥