InfoView reports for verified tensor transformations

einops? inspects the current target without changing it. Recognized operations appear in a compact InfoView panel. Checked types and the principal shape transformation remain visible. Independent disclosure sections expose the checked axes, proof obligations, lowering stages, generated execution, static work estimates, and correctness theorems on demand.

The tactic never evaluates or benchmarks user terms during elaboration.

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

Report checked types and shapes, verified lowering stages, generated execution, static work estimates, and compiler-correctness theorems found in the current target.

The tactic is observational: it does not change the target, add local facts, evaluate user terms, or run benchmarks. Symbolic certificates receive exact formulas without invented concrete dimensions.