diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
index d230ee2755..20eafdace4 100644
--- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean
+++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean
@@ -72,6 +72,7 @@ where
       let val  ← lemma.getValue
       let type ← inferType val
       let (xs, bis, type) ← forallMetaTelescopeReducing type
+      let type ← instantiateMVars type
       let lhs ← getLHS lemma.kind type
       if (← isDefEq lhs e) then
         unless (← synthesizeArgs lemma.getName xs bis discharge?) do
diff --git a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
index 0b017b0325..31e6ce2774 100644
--- a/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
+++ b/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
@@ -73,7 +73,7 @@ private partial def isPerm : Expr → Expr → MetaM Bool
   | s, t => s == t
 
 def mkSimpLemmaCore (e : Expr) (val : Expr) (post : Bool) (prio : Nat) (name? : Option Name) : MetaM SimpLemma := do
-  let type ← inferType e
+  let type ← instantiateMVars (← inferType e)
   unless (← isProp type) do
     throwError! "invalid 'simp', proposition expected{indentExpr type}"
   withNewMCtxDepth do