simp gets stuck on autoParam

[kim-em]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

simp gets stuck on autoParam hypotheses:

example (h : False := by trivial) : False := by
  simp at h

This used to work, but only because of the default (config := {decide := true}) behaviour of simp.

Context

This worked prior to #2722.

I'm making this issue as a placeholder I can link to when working around this in Mathlib.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.