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