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

State before:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a
neq : x ≠ a.back' hemp
⊢ x ∈ a.pop
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)
neq : x ≠ a.back' hemp
⊢ x ∈ a.pop

State before:
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
neq : x ≠ a.back' hemp
⊢ x ∈ a.pop
Tactic:
cases (Array.mem_push _ _ _).mp mem with
| inl mem => exact mem
| inr eq => exact absurd eq neq
State after:
no goals

State before:
case inl
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem✝ : x ∈ a.pop.push (a.back' hemp)
neq : x ≠ a.back' hemp
mem : x ∈ a.pop
⊢ x ∈ a.pop
Tactic:
exact mem
State after:
no goals

State before:
case inr
α : Type u_1
a : Array α
x : α
hemp : ¬a.isEmpty = true
mem : x ∈ a.pop.push (a.back' hemp)
neq : x ≠ a.back' hemp
eq : x = a.back' hemp
⊢ x ∈ a.pop
Tactic:
exact absurd eq neq
State after:
no goals