Verified tensor proof automation

This module is the public entry point for the einops proof tactic and the einops? InfoView report. The proof engine and report renderer live in separate modules so clients that only need proof automation do not depend on the widget implementation.