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

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr x : Array α
a : α
IH : (map f x).data = List.map f x.data
⊢ (map f (push x a)).data = List.map f (push x a).data
Tactic:
simp only [map_push, push_data, IH, List.map_append]
State after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr x : Array α
a : α
IH : (map f x).data = List.map f x.data
⊢ List.map f x.data ++ [f a] = List.map f x.data ++ List.map f [a]

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
arr x : Array α
a : α
IH : (map f x).data = List.map f x.data
⊢ List.map f x.data ++ [f a] = List.map f x.data ++ List.map f [a]
Tactic:
rfl
State after:
no goals