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

State before:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ a ∈ as ↔ a ∈ as.data
Tactic:
show as.any (fun b => a = b) = true ↔ a ∈ as.data
State after:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ any as (fun b => decide (a = b)) 0 (size as) = true ↔ a ∈ as.data

State before:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ any as (fun b => decide (a = b)) 0 (size as) = true ↔ a ∈ as.data
Tactic:
rewrite [any_eq_any_data]
State after:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (List.any as.data fun b => decide (a = b)) = true ↔ a ∈ as.data

State before:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (List.any as.data fun b => decide (a = b)) = true ↔ a ∈ as.data
Tactic:
simp only [List.any_eq_true, List.mem_iff_get]
State after:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) ↔ ∃ n, List.get as.data n = a

State before:
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) ↔ ∃ n, List.get as.data n = a
Tactic:
constructor
State after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) → ∃ n, List.get as.data n = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true

State before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) → ∃ n, List.get as.data n = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Tactic:
. intro h
  let ⟨_, ⟨i,hi⟩, h⟩ := h
  cases of_decide_eq_true h
  exact ⟨i,hi⟩
State after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Tactic:
. intro h; exists a; simp; exact h
State after:
no goals

State before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true) → ∃ n, List.get as.data n = a
Tactic:
intro h
State after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
⊢ ∃ n, List.get as.data n = a

State before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
⊢ ∃ n, List.get as.data n = a
Tactic:
let ⟨_, ⟨i,hi⟩, h⟩ := h
State after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h✝ : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
w✝ : α
i : Fin (List.length as.data)
hi : List.get as.data i = w✝
h : decide (a = w✝) = true
⊢ ∃ n, List.get as.data n = a

State before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h✝ : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
w✝ : α
i : Fin (List.length as.data)
hi : List.get as.data i = w✝
h : decide (a = w✝) = true
⊢ ∃ n, List.get as.data n = a
Tactic:
cases of_decide_eq_true h
State after:
case mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h✝ : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
i : Fin (List.length as.data)
hi : List.get as.data i = a
h : decide (a = a) = true
⊢ ∃ n, List.get as.data n = a

State before:
case mp.refl
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h✝ : ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
i : Fin (List.length as.data)
hi : List.get as.data i = a
h : decide (a = a) = true
⊢ ∃ n, List.get as.data n = a
Tactic:
exact ⟨i,hi⟩
State after:
no goals

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
⊢ (∃ n, List.get as.data n = a) → ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Tactic:
intro h
State after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ ∃ x, (∃ n, List.get as.data n = x) ∧ decide (a = x) = true
Tactic:
exists a
State after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ (∃ n, List.get as.data n = a) ∧ decide (a = a) = true

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ (∃ n, List.get as.data n = a) ∧ decide (a = a) = true
Tactic:
simp
State after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ ∃ n, List.get as.data n = a

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
as : Array α
h : ∃ n, List.get as.data n = a
⊢ ∃ n, List.get as.data n = a
Tactic:
exact h
State after:
no goals