Commit 2025-10-23 14:48 725562e7

View on Github →

refactor: make PosMulMono and alike custom classes (#29395) In the current setup, users get confusing non-beta-reduced goals involving a subtype when trying to provide an instance of PosMulMono. This PR changes it to be a custom structure with the expected fields. This follows PosSMulMono and alike.

Estimated changes

modified theorem mul_le_mul_of_nonneg_left
modified theorem mul_le_mul_of_nonneg_right
modified theorem mul_lt_mul_of_pos_left
modified theorem mul_lt_mul_of_pos_right