no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
a : α
as : List α
⊢ pointwise f (a :: as) [] = map (fun a => f a default) (a :: as)
simp only [pointwise_nil as, pointwise, eq_self_iff_true, and_self_iff, List.map]