`BookProof.ChapterSolovayCoordinates.tailTensorEquiv_map` : Measure.map tailTensorEquiv (coordinateTailMeasure.prod coordinateTailMeasure) = coordinateTailMeasure

Initializing...

`BookProof.ChapterSolovayCoordinates.tailTensorEquiv_map` : Measure.map tailTensorEquiv (coordinateTailMeasure.prod coordinateTailMeasure) = coordinateTailMeasure · Prove2Me