. rintro ⟨⟨i,hi⟩,ha⟩
  simp only [length_ofFn] at hi
  exact ⟨⟨i,hi⟩, ha⟩
case mp
α : 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

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
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