A tactic for beta reduction

Stream: Is there code for X?

[Snir Broshi]

Is there a tactic that only does beta reduction? I usually reach for dsimp only but it doesn't always work:

/-- error: `dsimp` made no progress -/
#guard_msgs in
theorem foo {f : True → Prop} :
    f ((fun n ↦ trivial) 0) ↔ f ((fun n ↦ trivial) 0) := by
  dsimp only
  sorry

Even if this is a bug in dsimp or if there's a technical reason why we shouldn't beta-reduce functions whose argument is a proof term, I'd still love to know of a dedicated tactic.
It feels strange to use a massive simplifier and disable its features just to get beta-reduction, it always looks like a non-terminal simp. Also dsimp only is pretty long to type.
I saw some strange beta% syntax once but I think it's some magic for term-mode and not a tactic.
Thanks!

[Matt Diamond]

beta_reduce?