Theorem: Array.mem_iff_mem_data (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ a ∈ x ↔ a ∈ x.data
Tactic:
induction x using cons_induction with
| empty =>
  simp only [not_mem_empty, data_toArray, List.not_mem_nil]
| cons v x IH =>
  rw [mem_cons, data_cons, List.mem_cons, IH]
State after:
no goals

State before:
case empty
α : Type u
inst✝ : DecidableEq α
a : α
⊢ a ∈ #[] ↔ a ∈ #[].data
Tactic:
simp only [not_mem_empty, data_toArray, List.not_mem_nil]
State after:
no goals

State before:
case cons
α : Type u
inst✝ : DecidableEq α
a v : α
x : Array α
IH : a ∈ x ↔ a ∈ x.data
⊢ a ∈ cons v x ↔ a ∈ (cons v x).data
Tactic:
rw [mem_cons, data_cons, List.mem_cons, IH]
State after:
no goals