X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < List.length (toList s) - 1
⊢ IsMaximal (List.get (toList s) { val := i, isLt := (_ : i < List.length (toList s)) })
    (List.get (toList s) { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) })
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (i : ℕ) (h : i < List.length (toList s) - 1),
    IsMaximal (List.get (toList s) { val := i, isLt := (_ : i < List.length (toList s)) })
      (List.get (toList s) { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) })
intro i hi
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < List.length (toList s) - 1
⊢ IsMaximal
    (series s
      (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i, isLt := (_ : i < List.length (toList s)) }))
    (series s
      (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) }))
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < List.length (toList s) - 1
⊢ IsMaximal (List.get (toList s) { val := i, isLt := (_ : i < List.length (toList s)) })
    (List.get (toList s) { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) })
simp only [toList, List.get_ofFn]
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi✝ : i < List.length (toList s) - 1
hi : i < s.length + 1 - 1
⊢ IsMaximal
    (series s
      (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i, isLt := (_ : i < List.length (toList s)) }))
    (series s
      (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) }))
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < List.length (toList s) - 1
⊢ IsMaximal
    (series s
      (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i, isLt := (_ : i < List.length (toList s)) }))
    (series s
      (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) }))
rw [length_toList] at hi
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi✝ : i < List.length (toList s) - 1
hi : i < s.length + 1 - 1
⊢ IsMaximal
    (series s
      (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i, isLt := (_ : i < List.length (toList s)) }))
    (series s
      (↑(Fin.cast (_ : List.length (List.ofFn s.series) = s.length + 1))
        { val := i + 1, isLt := (_ : Nat.succ i < List.length (toList s)) }))
exact s.step ⟨i, hi⟩