From 2bc44f63b2562722c70af066d5f86dc584636d66 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sat, 17 Feb 2024 05:41:48 -0800
Subject: [PATCH] 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 |  1 +
 tests/lean/run/3257.lean               | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 tests/lean/run/3257.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 8a59cd3cc149..63890e5e179b 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/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
diff --git a/tests/lean/run/3257.lean b/tests/lean/run/3257.lean
new file mode 100644
index 000000000000..cd35fd92b645
--- /dev/null
+++ b/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]