case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ↑{ val := ↑(Fin.last (eraseTop s).length), isLt := (_ : ↑(Fin.last (eraseTop s).length) < s.length + 1) } =
    ↑{ val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ { val := ↑(Fin.last (eraseTop s).length), isLt := (_ : ↑(Fin.last (eraseTop s).length) < s.length + 1) } =
    { val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }
ext
no goals
case h
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ↑{ val := ↑(Fin.last (eraseTop s).length), isLt := (_ : ↑(Fin.last (eraseTop s).length) < s.length + 1) } =
    ↑{ val := s.length - 1, isLt := (_ : s.length - 1 < s.length + 1) }
simp only [eraseTop_length, Fin.val_last, Fin.coe_castSucc, Fin.coe_ofNat_eq_mod,
  Fin.val_mk]