Commit 2026-05-11 12:09 260979c9

chore(Logic/Function/Basic): avoid defeq abuse of Set α = α → Prop in Cantor's theorem (#39147) #6114 and #35752 removed the defeq abuse in Function.cantor_surjective, then #35239 golfed it, reintroducing defeq abuse. This reverts the golf to avoid defeq abuse, and cleans up a bit.