simp only [get_ofFn]
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, get (ofFn f) n_1 = a) ↔ ∃ i, f i = a
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a) ↔ ∃ i, f i = a