Theorem: Array.mem_pop_or_eq_of_mem (RegexCorrectness/Data/Array.lean)

State before:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a
⊢ x ∈ a.pop ∨ x = a.back' hemp
Tactic:
rw [←Array.push_pop_eq a hemp] at mem
State after:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
⊢ x ∈ a.pop ∨ x = a.back' hemp

State before:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
⊢ x ∈ a.pop ∨ x = a.back' hemp
Tactic:
exact (Array.mem_push _ _ _).mp mem
State after:
no goals