Theorem: ArraySet.contains_iff (Aoc2023/Utils.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
⊢ contains as x = true ↔ x ∈ as
Tactic:
rw [contains]
State after:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
⊢ Array.contains as.content x = true ↔ x ∈ as

State before:
α : Type u_1
inst✝ : DecidableEq α
as : ArraySet α
x : α
⊢ Array.contains as.content x = true ↔ x ∈ as
Tactic:
exact Array.contains_def
State after:
no goals