diff --git a/Mathlib/Tactic/FastInstance.lean b/Mathlib/Tactic/FastInstance.lean
index 7a2f24d0c68348..3af61e032a5ab9 100644
--- a/Mathlib/Tactic/FastInstance.lean
+++ b/Mathlib/Tactic/FastInstance.lean
@@ -102,8 +102,8 @@ partial def makeFastInstance (inst expectedType : Expr) (trace : Array Name := #
         mvarId.assign (← makeFastInstance arg argExpectedType (trace := trace'))
       else
         -- For data fields, make sure that the lambda binders have the right type.
-        forallTelescopeReducing argExpectedType fun xs _ ↦ do
-          mvarId.assign <| ← mkLambdaFVars xs (arg.beta xs)
+        mvarId.assign <| ← forallTelescopeReducing argExpectedType fun xs _ ↦ do
+          mkLambdaFVars xs (← whnfI (mkAppN arg xs))
     return mkAppN f (← mvars.mapM instantiateMVars)
 
 /--
diff --git a/MathlibTest/InferInstanceAsPercent.lean b/MathlibTest/InferInstanceAsPercent.lean
index 177ad275bbb621..e86e263fa2b193 100644
--- a/MathlibTest/InferInstanceAsPercent.lean
+++ b/MathlibTest/InferInstanceAsPercent.lean
@@ -35,7 +35,7 @@ instance myNatInv_fixed : MyInv MyNat :=
 -- The binder type is `MyNat`:
 /--
 info: @[implicit_reducible] def myNatInv_fixed : MyInv MyNat :=
-{ myInv := fun (a : MyNat) => a + 1 }
+{ myInv := fun (a : MyNat) => (Nat.add a 0).succ }
 -/
 #guard_msgs in
 #print myNatInv_fixed