diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index 8bcb1ac7e3..2056ebcf40 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -67,7 +67,7 @@ where
       let val  ← lemma.getValue
       let type ← inferType val
       let (xs, bis, type) ← forallMetaTelescopeReducing type
-      let type ← instantiateMVars type
+      let type ← whnf (← instantiateMVars type)
       let lhs := type.appFn!.appArg!
       if (← isDefEq lhs e) then
         unless (← synthesizeArgs lemma.getName xs bis discharge?) do
diff --git a/tests/lean/run/simpRwBug.lean b/tests/lean/run/simpRwBug.lean
new file mode 100644
index 0000000000..bf2d440d40
--- /dev/null
+++ b/tests/lean/run/simpRwBug.lean
@@ -0,0 +1,4 @@
+open Nat
+
+theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) :=
+  Nat.recOn (motive := fun k => m + n + k = m + (n + k)) k rfl (fun k ih => by simp [Nat.add_succ, ih]; done)