Option that is some, let and case of cause rewriter not to simplify

Question

In Isabelle, I have to following proof state:

proof (prove)
using this:
  find (λc. length c = 1) f = Some [l]

goal (1 subgoal):
 1. fst (units_propagate f) = fst (units_propagate (update_formula f (atom_of l) (is_pos l)))

I'm pretty sure this is true, if you combine the hypothesis with some simplification. To illustrate this, I can rewrite the units_propagate f call using HOL-Library.Rewrite:

apply(rewrite at "units_propagate f" units_propagate.simps)
===========================================================
proof (prove)
goal (1 subgoal):
 1. find (λc. length c = 1) f = Some [l] ⟹
    fst (case find (λc. length c = 1) f of None ⇒ (f, Map.empty)
         | Some [l] ⇒
             let (f', e) = units_propagate (update_formula f (atom_of l) (is_pos l))
             in (f', e(atom_of l ↦ is_pos l))) =
    fst (units_propagate (update_formula f (atom_of l) (is_pos l)))

Now I'm pretty sure that if you use the hypothesis, the case of expression would simplify to only the Some case. Then, the use of fst allows keeping only the first element of the tuple, leading to the following proof state (hypothetical, as I cannot produce it):

proof (prove)
goal (1 subgoal):
 1. find (λc. length c = 1) f = Some [l] ⟹
    fst (units_propagate (update_formula f (atom_of l) (is_pos l))) =
    fst (units_propagate (update_formula f (atom_of l) (is_pos l)))

And clearly this is equal. Since I can write these steps down, I'd expect that a call of simp should be able to solve it. But it cannot. Using try, after a relatively long time, it finds the following invocation:

by (metis (no_types, lifting) case_prod_unfold fst_conv list.simps(4) list.simps(5) option.simps(5)) 

And that works. But this was quite painful and I don't understand it. Can someone shed a light upon why this is difficult?

My suspicion is that Isabelle is having trouble unifying the = Some [l] assumption with the l created in the process of simplifying away the case of expression. But I don't know how I would indicate to Isabelle that these two variables should be merged. In case it matters, here is the full definition of units_propagate:

function (sequential) units_propagate :: "'a formula ⇒ 'a formula × 'a env" where
"units_propagate f =
  (case find (λc. length c = 1) f of
      Some [l] ⇒ 
        let (f', e) = units_propagate (update_formula f (atom_of l) (is_pos l)) in
        (f', e(atom_of l ↦ is_pos l))
    | None ⇒ (f, Map.empty)
)"
  by(simp_all)
termination
  apply(relation "measure size_formula")
   apply(simp)
  using update_formula_decreases_units_propagate by auto

EDIT: Okay, after staring at the metis call a bit I managed to mangle it into the following proof script for inspection:

    apply(simp only: case_prod_unfold)
    apply(simp only: option.simps)
    apply(simp only: list.simps)
    apply(meson fstI)
    done

And indeed it seems to peel of all the data types layer by layer. But I feel like normally isabelle has no problem punching through my layering of datatypes. But here it seems hard. Can someone explain why? Is there a way to restructure my function in a way that isabelle has an easier time with it?