fix(rw??): whnf on equality hypotheses (#31609)

This PR adds some missing `whnf` in the `rw??` implementation. This only affects the behaviour of rewriting with local variables.

I discovered that sometimes the type can be an uninstantiated metavariable that needs to first instantiated, for example by using `whnf`.

Author: JovanGerb

Mathlib/Tactic/Widget/LibraryRewrite.lean

@@ -148,10 +148,10 @@ def addRewriteEntry (name : Name) (cinfo : ConstantInfo) :
 
 /-- Try adding the local hypothesis to the `RefinedDiscrTree`. -/
 def addLocalRewriteEntry (decl : LocalDecl) :
-    MetaM (List ((FVarId × Bool) × List (Key × LazyEntry))) :=
-  withReducible do
-  let (_, _, eqn) ← forallMetaTelescope decl.type
-  let some (lhs, rhs) := eqOrIff? eqn | return []
+    MetaM (List ((FVarId × Bool) × List (Key × LazyEntry))) := do
+  -- The transparency is set to `reducible`. Stronger reduction may give unexpected results.
+  let (_, _, eqn) ← forallMetaTelescopeReducing decl.type
+  let some (lhs, rhs) := eqOrIff? (← whnf eqn) | return []
   let result := ((decl.fvarId, false), ← initializeLazyEntryWithEta lhs)
   return [result, ((decl.fvarId, true), ← initializeLazyEntryWithEta rhs)]
 
@@ -213,8 +213,9 @@ structure Rewrite where
 def checkRewrite (thm e : Expr) (symm : Bool) : MetaM (Option Rewrite) := do
   withTraceNodeBefore `rw?? (return m!
     "rewriting {e} by {if symm then "← " else ""}{thm}") do
-  let (mvars, binderInfos, eqn) ← forallMetaTelescope (← inferType thm)
-  let some (lhs, rhs) := eqOrIff? eqn | return none
+  let (mvars, binderInfos, eqn) ← forallMetaTelescopeReducing (← inferType thm)
+  let some (lhs, rhs) := eqOrIff? (← whnf eqn) |
+    throwError "Expected equation, not {indentExpr eqn}"
   let (lhs, rhs) := if symm then (rhs, lhs) else (lhs, rhs)
   let unifies ← withTraceNodeBefore `rw?? (return m! "unifying {e} =?= {lhs}")
     (withReducible (isDefEq lhs e))
@@ -267,7 +268,8 @@ def getModuleRewrites (e : Expr) : MetaM (Array (Array (Rewrite × Name))) := do
 /-! ### Rewriting by hypotheses -/
 
 /-- Construct the `RefinedDiscrTree` of all local hypotheses. -/
-def getHypotheses (except : Option FVarId) : MetaM (RefinedDiscrTree (FVarId × Bool)) := do
+def getHypotheses (except : Option FVarId) : MetaM (RefinedDiscrTree (FVarId × Bool)) :=
+  withReducible do
   let mut tree : PreDiscrTree (FVarId × Bool) := {}
   for decl in ← getLCtx do
     if !decl.isImplementationDetail && except.all (· != decl.fvarId) then
@@ -429,8 +431,8 @@ def getRewriteInterfaces (e : Expr) (occ : Option Nat) (loc : Option Name) (exce
 /-- Render the matching side of the rewrite lemma.
 This is shown at the header of each section of rewrite results. -/
 def pattern {α} (type : Expr) (symm : Bool) (k : Expr → MetaM α) : MetaM α := do
-  forallTelescope type fun _ e => do
-    let some (lhs, rhs) := eqOrIff? e | throwError "Expected equation, not {indentExpr e}"
+  forallTelescopeReducing type fun _ e => do
+    let some (lhs, rhs) := eqOrIff? (← whnf e) | throwError "Expected equation, not {indentExpr e}"
     k (if symm then rhs else lhs)
 
 /-- Render the given rewrite results. -/