case mk
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi : i < n
⊢ get (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := hi }
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : Fin n
⊢ get (ofFn f) i = f i
cases' i with i hi
case mk
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi : i < n
⊢ get (ofFn f) { val := i, isLt := hi } =
    List.get (List.ofFn f) { val := i, isLt := (_ : i < List.length (List.ofFn f)) }
case mk
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi : i < n
⊢ get (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := hi }
conv_rhs => erw [← List.get_ofFn f ⟨i, by simpa using hi⟩]
case mk
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi : i < n
⊢ List.get (toList (ofFn f)) (↑(Fin.cast (_ : n = List.length (toList (ofFn f)))) { val := i, isLt := hi }) =
    List.get (List.ofFn f) { val := i, isLt := (_ : i < List.length (List.ofFn f)) }
case mk
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi : i < n
⊢ get (ofFn f) { val := i, isLt := hi } =
    List.get (List.ofFn f) { val := i, isLt := (_ : i < List.length (List.ofFn f)) }
simp only [get_eq_get]
no goals
case mk
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi : i < n
⊢ List.get (toList (ofFn f)) (↑(Fin.cast (_ : n = List.length (toList (ofFn f)))) { val := i, isLt := hi }) =
    List.get (List.ofFn f) { val := i, isLt := (_ : i < List.length (List.ofFn f)) }
congr <;> simp [Fin.heq_ext_iff]
no goals
n✝ : ℕ
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi : i < n
⊢ i < List.length (List.ofFn f)
simpa using hi