Commit 2024-12-18 19:47 933ad549

View on Github →

chore(Logic/ExistsUnique): amend usages of existsUnique to follow naming convention (#20028) As a definition ExistsUnique, the spelling of usages should be existsUnique rather than exists_unique. The majority of applications already conform to this (96), but there are some (30) exceptions. This PR fixes those. The large import is the import of Tactic.Alias to Logic.ExistsUnique, and is necessary if deprecations are to be performed here.

Estimated changes

added theorem CharP.existsUnique
deleted theorem CharP.exists_unique
added theorem Int.existsUnique_equiv
deleted theorem Int.exists_unique_equiv
added theorem existsUnique_const
added theorem existsUnique_eq'
added theorem existsUnique_eq
added theorem existsUnique_false
added theorem existsUnique_prop
deleted theorem exists_unique_const
deleted theorem exists_unique_eq'
deleted theorem exists_unique_eq
deleted theorem exists_unique_false
deleted theorem exists_unique_iff_exists
deleted theorem exists_unique_prop
deleted theorem unique_iff_exists_unique