From edb203ca5489187d4e3ff2063aad41266cbe396b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 May 2021 20:40:26 -0700
Subject: [PATCH] fix: fixes #481

---
 src/Lean/Meta/Tactic/Simp/SimpLemmas.lean | 1 +
 tests/lean/run/481.lean                   | 5 +++++
 2 files changed, 6 insertions(+)
 create mode 100644 tests/lean/run/481.lean

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