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

State before:
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
⊢ x ∈ a
Tactic:
cases decEq a.isEmpty true with
| isTrue hemp =>
  have := (Array.isEmpty_iff).mp hemp
  subst this
  simp at mem
| isFalse hemp =>
  rw [←Array.push_pop_eq a hemp]
  apply (Array.mem_push _ _ _).mpr
  exact Or.inl mem
State after:
no goals

State before:
case isTrue
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : a.isEmpty = true
⊢ x ∈ a
Tactic:
have := (Array.isEmpty_iff).mp hemp
State after:
case isTrue
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : a.isEmpty = true
this : a = #[]
⊢ x ∈ a

State before:
case isTrue
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : a.isEmpty = true
this : a = #[]
⊢ x ∈ a
Tactic:
subst this
State after:
case isTrue
α : Type u_1
x : α
mem : x ∈ #[].pop
hemp : #[].isEmpty = true
⊢ x ∈ #[]

State before:
case isTrue
α : Type u_1
x : α
mem : x ∈ #[].pop
hemp : #[].isEmpty = true
⊢ x ∈ #[]
Tactic:
simp at mem
State after:
no goals

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

State before:
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a.pop.push (a.back' hemp)
Tactic:
apply (Array.mem_push _ _ _).mpr
State after:
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a.pop ∨ x = a.back' hemp

State before:
case isFalse
α : Type u_1
a : Array α
x : α
mem : x ∈ a.pop
hemp : ¬a.isEmpty = true
⊢ x ∈ a.pop ∨ x = a.back' hemp
Tactic:
exact Or.inl mem
State after:
no goals