Native index normalization for generated einsum outputs

This module removes native-to-natural conversion round trips after output coordinates have been substituted into a generated kernel. The simplifier is restricted to compiler-generated coordinates, index bases, tensor reads, and their dependent bound proofs; user scalar expressions are left untouched.

def TorchLean.Tensor.Internal.Elab.Impl.nativeOutputIndexSimpContexts : Lean.MetaM (Lean.Meta.Simp.Context × Lean.Meta.Simp.Context)

Build the focused simplifier contexts used before and after output-coordinate substitution.

The first context preserves coordinate wrappers so selected generated lets can be unfolded explicitly. The second also performs iota reduction after a native coordinate has been substituted.

def TorchLean.Tensor.Internal.Elab.Impl.simplifyNativeOutputIndices (context : Lean.Meta.Simp.Context) (body : Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)

Normalize native indices throughout a completed generated output expression and return an equality from the normalized expression to the original one.

def TorchLean.Tensor.Internal.Elab.Impl.simplifyNativeProductIndices (baseContext : Lean.Meta.Simp.Context) (leadingLocals : Array Lean.Expr) (product : Lean.Expr) : Lean.Elab.TermElabM (Lean.Expr × Option Lean.Expr)

Normalize generated native indices in one scalar product after its output-axis lets have been opened.