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

State before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x)[0] = a
Tactic:
show (cons a x).val[0]'((cons a x).size_eq.symm ▸ hi) = a
State after:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x).val[0] = a

State before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ (cons a x).val[0] = a
Tactic:
simp only [Array.getElem_eq_data_get]
State after:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ List.get (cons a x).val.data { val := 0, isLt := (_ : 0 < Array.size (cons a x).val) } = a

State before:
α : Type u
β : Type v
n : Nat
a : α
x : SizedArray α n
hi : 0 < n + 1
⊢ List.get (cons a x).val.data { val := 0, isLt := (_ : 0 < Array.size (cons a x).val) } = a
Tactic:
dsimp [cons]
State after:
no goals