diff --git a/src/Lean/Elab/Extra.lean b/src/Lean/Elab/Extra.lean
index 73450fbc83..3346e79e5f 100644
--- a/src/Lean/Elab/Extra.lean
+++ b/src/Lean/Elab/Extra.lean
@@ -488,8 +488,10 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
     ```
     We can improve this failure in the future by applying default instances before reporting a type mismatch.
     -/
-    let lhs ← withRef stx[2] <| toTree stx[2]
-    let rhs ← withRef stx[3] <| toTree stx[3]
+    let lhsStx := stx[2]
+    let rhsStx := stx[3]
+    let lhs ← withRef lhsStx <| toTree lhsStx
+    let rhs ← withRef rhsStx <| toTree rhsStx
     let tree := .binop stx .regular f lhs rhs
     let r ← analyze tree none
     trace[Elab.binrel] "hasUncomparable: {r.hasUncomparable}, maxType: {r.max?}"
@@ -497,10 +499,10 @@ def elabBinRelCore (noProp : Bool) (stx : Syntax) (expectedType? : Option Expr)
       -- Use default elaboration strategy + `toBoolIfNecessary`
       let lhs ← toExprCore lhs
       let rhs ← toExprCore rhs
-      let lhs ← toBoolIfNecessary lhs
-      let rhs ← toBoolIfNecessary rhs
+      let lhs ← withRef lhsStx <| toBoolIfNecessary lhs
+      let rhs ← withRef rhsStx <| toBoolIfNecessary rhs
       let lhsType ← inferType lhs
-      let rhs ← ensureHasType lhsType rhs
+      let rhs ← withRef rhsStx <| ensureHasType lhsType rhs
       elabAppArgs f #[] #[Arg.expr lhs, Arg.expr rhs] expectedType? (explicit := false) (ellipsis := false) (resultIsOutParamSupport := false)
     else
       let mut maxType := r.max?.get!
diff --git a/tests/lean/binrelTypeMismatch.lean b/tests/lean/binrelTypeMismatch.lean
new file mode 100644
index 0000000000..fea4bee459
--- /dev/null
+++ b/tests/lean/binrelTypeMismatch.lean
@@ -0,0 +1,20 @@
+/-!
+# Testing that type mismatch errors for binary operations are localized to the LHS or RHS
+
+Before #3442, the error was placed on the entire expression than just the RHS.
+-/
+
+/-!
+When there's no max type, the ensureHasType failure is localized to the RHS.
+-/
+#check true = ()
+
+/-!
+When there's no max type, toBoolIfNecessary error is localized to LHS.
+-/
+#check ∀ (p : Prop), p == ()
+
+/-!
+When there's no max type, toBoolIfNecessary error is localized to RHS.
+-/
+#check ∀ (p : Prop), () == p
diff --git a/tests/lean/binrelTypeMismatch.lean.expected.out b/tests/lean/binrelTypeMismatch.lean.expected.out
new file mode 100644
index 0000000000..7a8b646d19
--- /dev/null
+++ b/tests/lean/binrelTypeMismatch.lean.expected.out
@@ -0,0 +1,20 @@
+binrelTypeMismatch.lean:10:14-10:16: error: type mismatch
+  ()
+has type
+  Unit : Type
+but is expected to have type
+  Bool : Type
+binrelTypeMismatch.lean:15:21-15:22: error: type mismatch
+  p
+has type
+  Prop : Type
+but is expected to have type
+  Bool : Type
+Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)
+binrelTypeMismatch.lean:20:27-20:28: error: type mismatch
+  p
+has type
+  Prop : Type
+but is expected to have type
+  Bool : Type
+Prop → sorryAx (Sort u_1) true : Sort (imax 1 u_1)