case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length = s.length

case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (i : Fin ((ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length + 1)),
    series (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))) i =
      series s
        (↑(Fin.cast
              (_ :
                Nat.succ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length =
                  Nat.succ s.length))
          i)
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s)) = s
refine' ext_fun _ _
no goals
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length = s.length
rw [length_ofList, length_toList, Nat.succ_sub_one]
case refine'_2.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length + 1
⊢ series (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))) { val := i, isLt := hi } =
    series s
      (↑(Fin.cast
            (_ :
              Nat.succ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length =
                Nat.succ s.length))
        { val := i, isLt := hi })
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
⊢ ∀ (i : Fin ((ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length + 1)),
    series (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))) i =
      series s
        (↑(Fin.cast
              (_ :
                Nat.succ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length =
                  Nat.succ s.length))
          i)
rintro ⟨i, hi⟩
no goals
case refine'_2.mk
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
i : ℕ
hi : i < (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length + 1
⊢ series (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))) { val := i, isLt := hi } =
    series s
      (↑(Fin.cast
            (_ :
              Nat.succ (ofList (toList s) (_ : toList s ≠ []) (_ : List.Chain' IsMaximal (toList s))).length =
                Nat.succ s.length))
        { val := i, isLt := hi })
simp [ofList, toList, -List.ofFn_succ]