no goals
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
(rw [pmap_eq_map_attach];
  exact ext_get (by simp) fun i hi1 hi2 => by
      simp [get_ofFn f ⟨i, hi1⟩])
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = pmap (fun i hi => f { val := i, isLt := hi }) (range n) (_ : ∀ (x : ℕ), x ∈ range n → x < n)
rw [pmap_eq_map_attach]
no goals
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ ofFn f = map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))
exact ext_get (by simp) fun i hi1 hi2 => by
    simp [get_ofFn f ⟨i, hi1⟩]
no goals
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
⊢ length (ofFn f) = length (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n)))
simp
no goals
α✝ : Type u
α : Type u_1
n : ℕ
f : Fin n → α
i : ℕ
hi1 : i < length (ofFn f)
hi2 : i < length (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n)))
⊢ get (ofFn f) { val := i, isLt := hi1 } =
    get (map (fun x => f { val := ↑x, isLt := (_ : ↑x < n) }) (attach (range n))) { val := i, isLt := hi2 }
simp [get_ofFn f ⟨i, hi1⟩]