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

State before:
α : Type u_1
a : Array α
x y : α
⊢ y ∈ a.push x ↔ y ∈ a ∨ y = x
Tactic:
unfold Array.push
State after:
α : Type u_1
a : Array α
x y : α
⊢ y ∈ { data := a.data.concat x } ↔ y ∈ a ∨ y = x

State before:
α : Type u_1
a : Array α
x y : α
⊢ y ∈ { data := a.data.concat x } ↔ y ∈ a ∨ y = x
Tactic:
simp [Array.mem_def]
State after:
no goals