Theorem: ArraySet.exists_getElem_of_mem (Aoc2023/Utils.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : x ∈ as
⊢ ∃ i, as.content[i] = x
Tactic:
rw [mem_def, Array.mem_def, List.mem_iff_get] at hx
State after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∃ n, List.get as.content.data n = x
⊢ ∃ i, as.content[i] = x

State before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
hx : ∃ n, List.get as.content.data n = x
⊢ ∃ i, as.content[i] = x
Tactic:
obtain ⟨i, hi⟩ := hx
State after:
case intro
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Fin (List.length as.content.data)
hi : List.get as.content.data i = x
⊢ ∃ i, as.content[i] = x

State before:
case intro
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Fin (List.length as.content.data)
hi : List.get as.content.data i = x
⊢ ∃ i, as.content[i] = x
Tactic:
refine ⟨i, ?_⟩
State after:
case intro
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Fin (List.length as.content.data)
hi : List.get as.content.data i = x
⊢ as.content[i] = x

State before:
case intro
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
i : Fin (List.length as.content.data)
hi : List.get as.content.data i = x
⊢ as.content[i] = x
Tactic:
rwa [← Array.getElem_eq_data_get] at hi
State after:
no goals