X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (List.length (toList s))
h : i < j
⊢ List.get (List.ofFn s.series) i < List.get (List.ofFn s.series) j
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (List.length (toList s))
h : i < j
⊢ List.get (toList s) i < List.get (toList s) j
dsimp [toList]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (List.length (toList s))
h : i < j
⊢ series s (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1)) i) <
    series s (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1)) j)
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (List.length (toList s))
h : i < j
⊢ List.get (List.ofFn s.series) i < List.get (List.ofFn s.series) j
rw [List.get_ofFn, List.get_ofFn]
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i j : Fin (List.length (toList s))
h : i < j
⊢ series s (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1)) i) <
    series s (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1)) j)
exact s.strictMono h