Theorem: Array.get?_data (Algorithm/Data/Classes/ToList.lean)

State before:
C : Type u_1
α : Type u_2
a : Array α
⊢ a.data.get? = a.get?
Tactic:
ext i
State after:
case h.a
C : Type u_1
α : Type u_2
a : Array α
i : ℕ
a✝ : α
⊢ a✝ ∈ a.data.get? i ↔ a✝ ∈ a.get? i

State before:
case h.a
C : Type u_1
α : Type u_2
a : Array α
i : ℕ
a✝ : α
⊢ a✝ ∈ a.data.get? i ↔ a✝ ∈ a.get? i
Tactic:
rw [Array.get?_eq_data_get?]
State after:
no goals