Theorem: Array.mem_push (Fifteen/Data/Array/Basic.lean)

State before:
α : Type u
inst✝ : DecidableEq α
a b : α
as : Array α
⊢ a ∈ push as b ↔ a ∈ as ∨ a = b
Tactic:
rw [mem_iff_mem_data, push_data, List.mem_append, mem_iff_mem_data, List.mem_singleton]
State after:
no goals