Proof automation for verified tensor transformations

einops closes tensor-layout goals with compiler-correctness theorems and general tensor laws. Equality between concrete rearrangements is reduced to equality of compact row-major index maps. Other goals use focused e-graphs, a deterministic simplification pass, and finally Mathlib's registered grind rules.

Every successful run produces an ordinary kernel-checked proof term. The tactic does not evaluate propositions through a separate native trust path. The e-graph normalizes proof terms; executable tensors continue to use the native Array lowerings.

partial def TorchLean.Tensor.Internal.instantiateOuterLets : Lean.Expr → Lean.Expr

Inline only the outer let chain of a generated term, exposing its lowering head without unfolding the lowering itself.

Not private, even though everything else in this section is: the einops? report decoders in Tactic/Report/ need the same traversal, and they used to get it from a byte-identical copy of these four lines in NN/Tactic/Einops/Report/Analysis/Common.lean. Report.Impl is nested in this namespace, so the uses over there resolve to this definition without any qualification.

checkedTransformShapes is not redefined here. Elab.Transform.View exports it, and this file now imports that module, which costs nothing: View's entire import closure was already inside this file's. The private copy that used to live here matched the original line for line, docstring included.

The open is needed because this file sits in TorchLean.Tensor.Internal while the elaborator helpers live one level down in Elab.Impl, so the name does not resolve on its own.

def TorchLean.Tensor.Internal.einopsTactic : Lean.ParserDescr

Close a tensor-layout identity using TorchLean.Tensor.Internal compiler-correctness theorems, the library's tensor algebra, and Mathlib's registered grind rules.