no goals
ι : Type ?u.427557
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ : List α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun l a => List.erase l (f a)) (map f l₁) l₂
induction l₂ generalizing l₁ <;> [rfl; simp only [foldl_cons, map_erase finj, *]]