rintro ⟨_,⟨h,rfl⟩,rfl⟩
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
x : α
⊢ (∃ a, (∃ h, { val := i, isLt := ⋯ } = a) ∧ f a = x) → ∃ h, f { val := i, isLt := ⋯ } = x
case intro.intro.intro
n : Nat
α : Type u_1
f : Fin n → α
i : Nat
h : i < List.length (List.fins n)
⊢ ∃ h_1, f { val := i, isLt := ⋯ } = f { val := i, isLt := ⋯ }