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

State before:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ a ∈ x ↔ ∃ i hi, x[i] = a
Tactic:
rewrite [mem_iff_mem_data, List.mem_iff_get]
State after:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, x[i] = a

State before:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, x[i] = a
Tactic:
simp only [getElem_eq_data_get]
State after:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, List.get x.data { val := i, isLt := hi } = a

State before:
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) ↔ ∃ i hi, List.get x.data { val := i, isLt := hi } = a
Tactic:
constructor
State after:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) → ∃ i hi, List.get x.data { val := i, isLt := hi } = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a

State before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) → ∃ i hi, List.get x.data { val := i, isLt := hi } = a

case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
Tactic:
. exact fun ⟨i,hxi⟩ => ⟨i.1,i.2,hxi⟩
State after:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
Tactic:
. exact fun ⟨i,hi,hxi⟩ => ⟨⟨i,hi⟩,hxi⟩
State after:
no goals

State before:
case mp
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ n, List.get x.data n = a) → ∃ i hi, List.get x.data { val := i, isLt := hi } = a
Tactic:
exact fun ⟨i,hxi⟩ => ⟨i.1,i.2,hxi⟩
State after:
no goals

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
a : α
x : Array α
⊢ (∃ i hi, List.get x.data { val := i, isLt := hi } = a) → ∃ n, List.get x.data n = a
Tactic:
exact fun ⟨i,hi,hxi⟩ => ⟨⟨i,hi⟩,hxi⟩
State after:
no goals