Commit 2025-11-29 00:17 63af23d7

View on Github →

chore: golf using contrapose for ↔ (#32193) This PR golfs some proofs to use the new ↔ support in the contrapose/contrapose! tactic.

Estimated changes

modified theorem le_inv_self_iff
modified theorem lt_inv_self_iff
modified theorem mul_self_le_one_iff
modified theorem mul_self_lt_one_iff