fix: simp fails to discharge autoParam premises even when it can …

…reduce them to `True` (#3314)

closes #3257

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -471,6 +471,7 @@ where
       return some mvarId
 
 def dischargeDefault? (e : Expr) : SimpM (Option Expr) := do
+  let e := e.cleanupAnnotations
   if isEqnThmHypothesis e then
     if let some r ← dischargeUsingAssumption? e then
       return some r

tests/lean/run/3257.lean

@@ -0,0 +1,18 @@
+structure T : Prop
+structure U : Prop
+
+theorem foo : T → U := λ _ => {}
+theorem bar : (_ : T := by trivial) → U := λ _ => {}
+
+-- fails as expected
+example : U := by
+  fail_if_success simp
+  sorry
+
+-- works as expected, discharging `T` via `T.mk`
+example : U := by
+  simp [foo, T.mk]
+
+example : U := by
+  set_option trace.Meta.Tactic.simp true in
+  simp [bar, T.mk]