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

State before:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ (push (cons a₁ x) a₂).val.data = (cons a₁ (push x a₂)).val.data
Tactic:
dsimp [push,cons, Array.push]
State after:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ List.concat (a₁ :: x.val.data) a₂ = a₁ :: List.concat x.val.data a₂

State before:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ List.concat (a₁ :: x.val.data) a₂ = a₁ :: List.concat x.val.data a₂
Tactic:
simp only [List.concat_eq_append]
State after:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ a₁ :: x.val.data ++ [a₂] = a₁ :: (x.val.data ++ [a₂])

State before:
α : Type u
β : Type v
n : Nat
a₁ a₂ : α
x : SizedArray α n
⊢ a₁ :: x.val.data ++ [a₂] = a₁ :: (x.val.data ++ [a₂])
Tactic:
rfl
State after:
no goals