`←` lifts over `&&` in `do` blocks, defeating short-circuiting

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

def bar : IO Bool := do
  IO.println "bar called"
  return true

def foo : Bool := false

def test₁ : IO Unit := do
  if foo && (← bar) then
    IO.println "branch taken"

-- bar called
#eval test₁

def test₂ : IO Unit := do
  if foo then
    if ← bar then
      IO.println "branch taken"

-- bar not called
#eval test₂

In this code, I expect that bar is not called in both cases (or, more precisely, that the monadic effect of bar does not happen) due to the short circuiting behavior of &&.

Context

This could be considered as a variant of #3713.

Steps to Reproduce

1. Copy the code above into live.lean-lang.org

Expected behavior: The monadic effect of bar is not observed.

Actual behavior: The monadic effect of bar is observed.

Versions

4.22.0-nightly-2025-06-17 on live.lean-lang.org

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal reproducer from the issue in live.lean-lang.org and compare test₁ with test₂, focusing on how ← is handled in the if foo && ... expression inside a do block. Done means the monadic effect of bar is not observed when foo is false, matching the nested-if example.