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

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

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

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