Theorem: Array.get_of_mem (LeanSAT/AIG/RelabelNat.lean)

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
⊢ a ∈ as → ∃ i, as[i] = a
Tactic:
intro ha
State after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
⊢ ∃ i, as[i] = a

State before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
⊢ ∃ i, as[i] = a
Tactic:
rcases List.get_of_mem ha.val with ⟨i, hi⟩
State after:
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
i : Fin as.data.length
hi : as.data.get i = a
⊢ ∃ i, as[i] = a

State before:
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
i : Fin as.data.length
hi : as.data.get i = a
⊢ ∃ i, as[i] = a
Tactic:
exists i
State after:
no goals