Theorem: SizedArray.mem_iff_get (Algdata/Data/Array/Sized.lean)

State before:
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ a ∈ x ↔ ∃ i, x[↑i] = a
Tactic:
rewrite [mem_iff_mem_val, Array.mem_iff_get]
State after:
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) ↔ ∃ i, x[↑i] = a

State before:
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) ↔ ∃ i, x[↑i] = a
Tactic:
constructor
State after:
case mp
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) → ∃ i, x[↑i] = a

case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a

State before:
case mp
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) → ∃ i, x[↑i] = a

case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a
Tactic:
. exact fun ⟨i,hi,hxi⟩ => ⟨⟨i, x.size_eq.symm ▸ hi⟩, hxi⟩
State after:
case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a
Tactic:
. exact fun ⟨i,hxi⟩ => ⟨i.1, x.size_eq.symm ▸ i.2, hxi⟩
State after:
no goals

State before:
case mp
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i hi, x.val[i] = a) → ∃ i, x[↑i] = a
Tactic:
exact fun ⟨i,hi,hxi⟩ => ⟨⟨i, x.size_eq.symm ▸ hi⟩, hxi⟩
State after:
no goals

State before:
case mpr
α : Type u
inst✝ : DecidableEq α
n : Nat
a : α
x : SizedArray α n
⊢ (∃ i, x[↑i] = a) → ∃ i hi, x.val[i] = a
Tactic:
exact fun ⟨i,hxi⟩ => ⟨i.1, x.size_eq.symm ▸ i.2, hxi⟩
State after:
no goals