Theorem: Array.mem_back' (RegexCorrectness/Data/Array.lean)

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.back' hemp ∈ a
Tactic:
simp [back', Array.mem_def, Array.getElem_eq_data_get]
State after:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.data.get ⟨a.size - 1, ⋯⟩ ∈ a.data

State before:
α : Type u_1
a : Array α
hemp : ¬a.isEmpty = true
⊢ a.data.get ⟨a.size - 1, ⋯⟩ ∈ a.data
Tactic:
apply List.get_mem
State after:
no goals