no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
b : β
bs : List β
⊢ pointwise f [] (b :: bs) = map (f default) (b :: bs)
simp only [nil_pointwise bs, pointwise, eq_self_iff_true, and_self_iff, map]