fix: assigned metavariables in SimpLemmas

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

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