no goals
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
l : List α₁
init : β
⊢ foldr g init (map f l) = foldr (fun x y => g (f x) y) init l
induction l generalizing init <;> simp [*]