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.

The lowering proof helpers and the einops? report decoders use this traversal.

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.