no goals
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
⊢ length (map g (ofFn f)) = length (ofFn (g ∘ f))
simp
no goals
α : Type u
β : Type u_1
n : ℕ
f : Fin n → α
g : α → β
i : ℕ
h : i < length (map g (ofFn f))
h' : i < length (ofFn (g ∘ f))
⊢ get (map g (ofFn f)) { val := i, isLt := h } = get (ofFn (g ∘ f)) { val := i, isLt := h' }
simp