simp fails to discharge auto_param premises even when it can reduce them to True

[JLimperg]

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 fails to discharge auto_param premises even when it can reduce the premise to True without running the auto_param tactic:

structure T : Prop
structure U : Prop

theorem foo : T → U := λ _ => {}
theorem bar : (_ : T := by trivial) → U := λ _ => {}

-- fails as expected
example : U := by
  simp

-- works as expected, discharging `T` via `T.mk`
example : U := by
  simp [foo, T.mk]

-- fails, failing to discharge `T` via `T.mk`
example : U := by
  set_option trace.Meta.Tactic.simp true in
  simp [bar, T.mk]
  -- [Meta.Tactic.simp.discharge] >> discharge?: autoParam T _auto
  -- [Meta.Tactic.simp.rewrite] { }:1000, T ==> True
  -- [Meta.Tactic.simp.discharge] bar, failed to discharge hypotheses autoParam T _auto

Context

Possibly related to #2243 and #2862.

Versions

4.6.0-rc1

Impact

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

[JLimperg]

🎉 Thanks!