diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 711c59de5348..c6c743d8006a 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -563,8 +563,12 @@ partial def instantiateExprMVars [Monad m] [MonadMCtx m] [STWorld ω m] [MonadLi
         let wasMVar := f.isMVar
         let f ← instantiateExprMVars f
         if wasMVar && f.isLambda then
-          /- Some of the arguments in args are irrelevant after we beta reduce. -/
-          instantiateExprMVars (f.betaRev args.reverse)
+          /- Some of the arguments in `args` are irrelevant after we beta
+             reduce. Also, it may be a bug to not instantiate them, since they
+             may depend on free variables that are not in the context (see
+             issue #4375). So we pass `useZeta := true` to ensure that they are
+             instantiated. -/
+          instantiateExprMVars (f.betaRev args.reverse (useZeta := true))
         else
           instArgs f
       match f with
diff --git a/tests/lean/4375.lean b/tests/lean/4375.lean
new file mode 100644
index 000000000000..16998f76b58f
--- /dev/null
+++ b/tests/lean/4375.lean
@@ -0,0 +1,5 @@
+example: Nat → Nat :=
+  let a : Nat := Nat.zero
+  fun (_ : Nat) =>
+    let b : Nat := Nat.zero
+    (fun (_ : a = b) => 0) (Eq.refl a)
diff --git a/tests/lean/4375.lean.expected.out b/tests/lean/4375.lean.expected.out
new file mode 100644
index 000000000000..e69de29bb2d1