Theorem: Array.mem_push (LeanSAT/Upstream/ToStd.lean)

State before:
α : Type u_1
A : Array α
x y : α
⊢ y ∈ push A x ↔ y ∈ A ∨ y = x
Tactic:
simp [push, Array.mem_def]
State after:
no goals