Theorem: Array.push_pop_back' (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ push (pop { data := l }) (back' { data := l } h) = { data := l }
Tactic:
simp only [back'_eq_data_getLast, pop, push, size, getElem_eq_data_get, List.concat_eq_append]
State after:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ { data := List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] } = { data := l }

State before:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ { data := List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] } = { data := l }
Tactic:
apply congrArg Array.mk
State after:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] = l

State before:
α : Type u
as : Array α
h✝ : size as > 0
l : List α
h : size { data := l } > 0
⊢ List.dropLast l ++ [List.getLast l (_ : { data := l }.data ≠ [])] = l
Tactic:
apply l.dropLast_concat_getLast
State after:
no goals