IR eta reduction/common subexpression elimination on Prods

Prerequisites

• 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

Decomposing a pair and then returning a pair of the components is a no-op that is not presently optimized away by the compiler pipeline.

Steps to Reproduce

/--
trace: [Compiler.saveMono] size: 3
    def projThenMk xy : Prod (Array Nat) (Array Nat) :=
      cases xy : Prod (Array Nat) (Array Nat)
      | Prod.mk fst snd =>
        let _x.1 := Prod.mk ◾ ◾ fst snd;
        return _x.1
-/
#guard_msgs in
set_option trace.Compiler.saveMono true in
def projThenMk (xy : Array Nat × Array Nat) : Array Nat × Array Nat :=
  let a : Array Nat := xy.fst
  let b : Array Nat := xy.snd
  (a, b)

Expected behavior: projThenMk should have been optimzed to the identity function. No pairs should be decomposed.

Actual behavior: The xy pair is decomposed and a fresh pair of its components is returned.

Versions

Lean 4.31.0-rc1
Target: x86_64-unknown-linux-gnu

Impact

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

Run the provided minimal reproduction with the Compiler.saveMono trace enabled and inspect how the pair projections and reconstruction are represented in the compiler pipeline. The change is done when projThenMk is optimized to the identity behavior, with no pair decomposition, and the trace-based guard confirms the improved result.