exists ⟨i, by rewrite [length_ofFn]; exact hi⟩
case mpr.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi : i < n
ha : f { val := i, isLt := hi } = a
⊢ ∃ n_1, f (Fin.cast (_ : length (ofFn f) = n) n_1) = a
no goals