diff --git a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
index ded27d304c..c2dfc71d72 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
@@ -153,6 +153,7 @@ private def mkSimpLemmaCore (e : Expr) (levelParams : Array Name) (proof : Expr)
   let type ← instantiateMVars (← inferType e)
   withNewMCtxDepth do
     let (xs, _, type) ← withReducible <| forallMetaTelescopeReducing type
+    let type ← whnfR type
     let (keys, perm) ←
       match type.eq? with
       | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs, ← isPerm lhs rhs)
diff --git a/tests/lean/run/481.lean b/tests/lean/run/481.lean
new file mode 100644
index 0000000000..b2445b67ab
--- /dev/null
+++ b/tests/lean/run/481.lean
@@ -0,0 +1,5 @@
+example (b : let n : Nat := 2; (n = 13)) : Bool := by
+  simp_all
+
+example (b : let n : Nat := 2; (n = 13)) : n + 1 = 14 := by
+  simp_all