Commit 2023-12-21 20:35 14c72960

View on Github →

chore(*): use ∃ x ∈ s, _ instead of ∃ (x) (_ : x ∈ s), _ (#9184) Search for [∀∃].*(_ and manually replace some occurrences with more readable versions. In case of ∀, the new expressions are defeq to the old ones. In case of ∃, they differ by exists_prop. In some rare cases, golf proofs that needed fixing.

Estimated changes

modified theorem Multiset.prod_eq_pow_single
modified theorem pow_le_one
modified theorem pow_lt_one
modified theorem Set.le_mulIndicator
modified theorem Set.mulIndicator_le_self'
modified theorem mem_balancedHull_iff
modified theorem subset_balancedCore
modified theorem Multiset.toFinset_nsmul
modified theorem Finset.strongInduction_eq
modified theorem Finset.inf'_mem
modified theorem Finset.inf_mem
modified theorem Finset.sup'_mem
modified theorem Finset.sup_mem
modified theorem List.prod_isUnit
modified theorem List.Chain'.tail
modified def List.prev
modified theorem MvPolynomial.mem_vars
modified def Semiquot.liftOn
modified theorem Set.Nontrivial.exists_lt
modified theorem Set.Nontrivial.pair_subset
modified theorem Set.mem_image
modified theorem Set.ordConnected_biInter
modified theorem Set.InjOn.image_biInter_eq
modified theorem Set.update_preimage_univ_pi
modified theorem Localization.liftOn_mk'
modified theorem Localization.liftOn_mk
modified theorem Localization.liftOn_zero
modified def Cycle.formPerm
modified def Subgroup.ofDiv