. exact fun ⟨i,hxi⟩ => ⟨i.1,i.2,hxi⟩
case mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) → ∃ i hi, List.get x.data { val := i, isLt := hi } = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a