Theorem: Array.map_cons (Algdata/Data/Array/Lemmas.lean)

State before:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
a : α
x : Array α
⊢ (map f (cons a x)).data = (cons (f a) (map f x)).data
Tactic:
simp only [map_data', cons]
State after:
α : Type u
m : Type v → Type w
inst✝ : Monad m
β : Type u_1
f : α → β
a : α
x : Array α
⊢ List.map f (a :: x.data) = f a :: List.map f x.data

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