Commit 2026-04-29 14:58 55a84ce3

View on Github →

chore(*): remove unnecessary parentheses around '' and ⁻¹' (#38626) This PR follows up on #38625 by removing parentheses around Set.image and Set.preimage operators that have become unnecessary due to the switch in associativity. This PR was generated by running the command rg " ('|⁻¹)'"' \([^)]*'"('|⁻¹)' " --vimgrep **/*.lean | sort -h | vim - and then in Vim running the macro:

gF
/ \('|⁻¹\)' (
f(
sd(

followed by

:w
:buf 1

on every match that manually looked to have the right form. I deleted a few more parentheses when they looked appropriate. Then I did another filtering pass with git add -p, adding only the changes that made sense.

Estimated changes

modified theorem Set.LeftInvOn.image_image'
modified theorem Set.LeftInvOn.image_image
modified theorem Set.SurjOn.image_preimage
modified theorem Set.image_comp
modified theorem Set.image_image
modified theorem Set.image_preimage_eq
modified theorem Set.image_preimage_eq_iff
modified theorem Set.image_preimage_subset
modified theorem Set.preimage_comp
modified theorem Set.preimage_image_eq
modified theorem Set.preimage_image_preimage
modified theorem Set.preimage_image_univ
modified theorem Set.preimage_inl_image_inr
modified theorem Set.preimage_inr_image_inl
modified theorem Set.subset_preimage_image
modified theorem Subtype.image_preimage_coe
modified theorem Subtype.image_preimage_val
modified theorem sigma_mk_preimage_image'
modified theorem Set.preimage_liftCover
modified theorem Equiv.image_preimage
modified theorem Equiv.image_symm_image
modified theorem Equiv.preimage_image
modified theorem Equiv.symm_image_image
modified theorem OrderIso.image_preimage
modified theorem OrderIso.image_symm_image
modified theorem OrderIso.preimage_image
modified theorem OrderIso.symm_image_image
modified theorem Homeomorph.image_preimage
modified theorem Homeomorph.preimage_image
modified theorem UniformEquiv.image_preimage
modified theorem UniformEquiv.preimage_image