rintro ⟨⟨i,hi⟩,ha⟩
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.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