exact ⟨⟨i,hi⟩, ha⟩
case mp.intro.mk
α : Type u
β : Type v
n : Nat
f : Fin n → α
a : α
i : Nat
hi✝ : i < length (ofFn f)
ha : f (Fin.cast (_ : length (ofFn f) = n) { val := i, isLt := hi✝ }) = a
hi : i < n
⊢ ∃ i, f i = a
no goals