How to create appropriate lemmas to prove this lemma in Isabelle?

fun intersperse :: " 'a list ⇒ 'a ⇒ 'a list" where
  "intersperse (x#y#xs) a = x#(a#(intersperse (y#xs) a))"|
  "intersperse xs _ = xs"

lemma target:"map f (intersperse xs a) = intersperse (map f xs) (f a)"

The lemma seems very intuitive, but I can't get Isabelle to prove the lemma. I tried induction on xs, but the sledgehammer still can't find a proof. Then I tried adding auxiliary lemmas, all of them are easy to prove but don't help much proving target. I will list my attempts below though:

lemma intersp_1: "interspserse (xs@[y,x]) a = (intersperse (xs@[y]) a) @ [a,x]"
...done

lemma intersp_2:"map f (intersperse (xs@[b,x]) a) = (map f (intersperse (xs@[b]) a)) @ [(f a),(f x)]"
...done

lemma intersp_3: "map f (intersperse (x#y#xs) a) = (f x)#(f a)#(map f (intersperse (y#xs) a))"
...done

As a new learner of Isabelle I'm kind of stuck here. The only solution that I can currently think of is to come up with an appropriate lemma that provides enough hint to the solver. However I don't know how to "appropriately" dispart the induction step of target (after applying induction on xs) into a supplementary lemma. The induction step is

goal (1 subgoal):
 1. ⋀aa xs.
       map f (intersperse xs a) = intersperse (map f xs) (f a) ⟹
       map f (intersperse (aa # xs) a) = intersperse (map f (aa # xs)) (f a)

Any help is appreciated!

Solution

Here's a proof:

lemma target: "map f (intersperse xs a) = intersperse (map f xs) (f a)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  consider "xs = []" | "∃y ys. xs = y # ys" by (meson list.exhaust)
  then show ?case using Cons by (cases; auto)
qed

The key here is that intersperse (x # []) a and intersperse (x # y # ys) a match different patterns, so by considering each case separately sledgehammer can easily find a proof.