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]