Commit 2026-08-11 15:45 4e9f33ff

chore: improve Set / Finset congruence API (#42640) These changes concern the following four equivalences:

variable {α β : Type*}
example (e : α ≃ β) : Set α ≃ Set β := Equiv.Set.congr e -- No change
example (e : α ≃ β) : Finset α ≃ Finset β := Equiv.finsetCongr e -- Rename to `Equiv.Finset.congr`
example {s t : Set α} (h : s = t) : s ≃ t := Equiv.setCongr h -- No change
example {s t : Finset α} (h : s = t) : s ≃ t := sorry -- Missing: add as `Equiv.finsetCongr`

In summary we essentially implement two changes:

1. Rename the existing Equiv.finsetCongr to Equiv.Finset.congr since it is currently inconsistent with both Equiv.Set.congr and Equiv.setCongr
2. Fill a gap by giving the the now-available Equiv.finsetCongr name to the Finset version of Equiv.setCongr