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

case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
⊢ ∀ (n : ℕ) (h₁ : n < List.length (toList (ofList l hl hc))) (h₂ : n < List.length l),
    List.get (toList (ofList l hl hc)) { val := n, isLt := h₁ } = List.get l { val := n, isLt := h₂ }
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
⊢ toList (ofList l hl hc) = l
refine' List.ext_get _ _
no goals
case refine'_1
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
⊢ List.length (toList (ofList l hl hc)) = List.length l
rw [length_toList, length_ofList,
  tsub_add_cancel_of_le (Nat.succ_le_of_lt <| List.length_pos_of_ne_nil hl)]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.get (toList (ofList l hl hc)) { val := i, isLt := hi } = List.get l { val := i, isLt := hi' }
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
⊢ ∀ (n : ℕ) (h₁ : n < List.length (toList (ofList l hl hc))) (h₂ : n < List.length l),
    List.get (toList (ofList l hl hc)) { val := n, isLt := h₁ } = List.get l { val := n, isLt := h₂ }
intro i hi hi'
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.get (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) { val := i, isLt := hi } =
    List.get l { val := i, isLt := hi' }
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.get (toList (ofList l hl hc)) { val := i, isLt := hi } = List.get l { val := i, isLt := hi' }
dsimp [ofList, toList]
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.nthLe l
      ↑(↑(Fin.cast
              (_ : List.length (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) = List.length l - 1 + 1))
          { val := i, isLt := hi })
      (_ :
        ↑(↑(Fin.cast
                  (_ :
                    List.length (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) = List.length l - 1 + 1))
              { val := i, isLt := hi }) <
          List.length l) =
    List.get l { val := i, isLt := hi' }
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.get (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) { val := i, isLt := hi } =
    List.get l { val := i, isLt := hi' }
rw [List.get_ofFn]
no goals
case refine'_2
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
l : List X
hl : l ≠ []
hc : List.Chain' IsMaximal l
i : ℕ
hi : i < List.length (toList (ofList l hl hc))
hi' : i < List.length l
⊢ List.nthLe l
      ↑(↑(Fin.cast
              (_ : List.length (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) = List.length l - 1 + 1))
          { val := i, isLt := hi })
      (_ :
        ↑(↑(Fin.cast
                  (_ :
                    List.length (List.ofFn fun i => List.nthLe l ↑i (_ : ↑i < List.length l)) = List.length l - 1 + 1))
              { val := i, isLt := hi }) <
          List.length l) =
    List.get l { val := i, isLt := hi' }
rfl