fix: normalize instance argument in getStuckMVar? for class projections (#12778)

This PR fixes an inconsistency in `getStuckMVar?` where the instance
argument to class projection functions and auxiliary parent projections
was not whnf-normalized before checking for stuck metavariables. Every
other case in `getStuckMVar?` (recursors, quotient recursors, `.proj`
nodes) normalizes the major argument via `whnf` before recursing — class
projection functions and aux parent projections were the exception.

This bug was identified by Matthew Jasper. When the instance parameter
to a class projection is not normalized, `getStuckMVar?` may fail to
detect stuck metavariables that would be revealed by whnf, or conversely
may report stuckness for expressions that would reduce to constructors.
This caused issues with `OfNat` and `Zero` at
`with_reducible_and_instances` transparency.

Note: PR #12701 (already merged) is also required to fix the original
Mathlib examples.

Author: leodemoura

src/Lean/Meta/WHNF.lean

@@ -348,7 +348,7 @@ mutual
             unless projInfo.fromClass do return none
             -- First check whether `e`s instance is stuck.
             if let some major := args[projInfo.numParams]? then
-              if let some mvarId ← getStuckMVar? major then
+              if let some mvarId ← getStuckMVar? (← whnf major) then
                 return mvarId
             /-
             Then, recurse on the explicit arguments
@@ -366,7 +366,7 @@ mutual
           else if let some auxInfo ← getAuxParentProjectionInfo? fName then
             unless auxInfo.fromClass do return none
             if let some major := args[auxInfo.numParams]? then
-              if let some mvarId ← getStuckMVar? major then
+              if let some mvarId ← getStuckMVar? (← whnf major) then
                 return mvarId
             return none
           else