refactor(Data): make Set a one-field structure

[YaelDillies]

Replace

def Set (α : Type u) := α → Prop

with

structure Set (α : Type u) where
  ofPred :: Mem : α → Prop

Generated by Claude Opus 4.8. Painfully reviewed and improved line-by-line by myself.

Assisted-by: Claude Opus 4.8

---

• depends on: chore: add missing noncomputable #41446
• depends on: chore(Data): rename setOf to Set.ofPred #41507
• depends on: refactor: notation for EventuallyEq on Set #41533

See previous attempt at #39211

[github-actions]

PR summary 9c730e85e9

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ AddAction.properVAdd_iff_isCompact_setOf_inter_nonempty
+ Antitone.countable_setOfPred_two_preimages
+ AntitoneOn.countable_setOfPred_two_preimages
+ ContinuousMap.dense_setOfPred_contDiff
+ Convex.setOfPred_const_imp
+ Convex.setOfPred_gauge_le
+ Countable.ofPred_finite
+ DefinableFun.ofPred_eq
+ DefinableFun.ofPred_eq_const
+ Equicontinuous.isClosed_setOfPred_tendsto
+ Filter.TotallyBounded.isCompact_setOfPred_clusterPt
+ Filter.TotallyBounded.totallyBounded_setOfPred_clusterPt
+ GeneratePiSystem
+ GenerateSetAlgebra
+ Ideal.setOfPred_isPrincipal_wellFoundedOn_gt
+ Indep.closure_eq_setOfPred_isBasis_insert
+ Indep.isBasis_setOfPred_insert_isBasis
+ IsAntichain.eq_setOfPred_maximal
+ IsAntichain.eq_setOfPred_minimal
+ IsClosed.setOfPred_mapsTo
+ IsGδ.setOfPred_continuousAt
+ IsGδ.setOfPred_irrational
+ IsGδ.setOfPred_liouville
+ IsHamiltonian.setOfPred_support
+ LHom.setOfPred_realize_onFormula
+ LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete
+ LinearOrderedAddCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete
+ LinearOrderedCommGroup.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete
+ LinearOrderedCommGroup.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete
+ LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_ge_gt_iff_nonempty_discrete_of_ne_zero
+ LinearOrderedCommGroupWithZero.wellFoundedOn_setOfPred_le_lt_iff_nonempty_discrete_of_ne_zero
+ MeasurableSet.setOfPred_finite
+ MeasurableSet.setOfPred_infinite
+ MemFP
+ MemFS
+ MemFiniteInterClosure
+ MemSpan
+ MemεClosure
+ MeromorphicOn.codiscreteWithin_setOfPred_ne_zero
+ Monotone.countable_setOfPred_two_preimages
+ MonotoneOn.countable_setOfPred_two_preimages
+ MulAction.properSMul_iff_isCompact_setOfPred_inter_nonempty
+ Nat.isSemilinearSet_setOfPred_eq
+ Nat.isSemilinearSet_setOfPred_mulVec_eq
+ ProperSMul.isCompact_setOfPred_inter_nonempty
+ ProperVAdd.isCompact_setOf_inter_nonempty
+ Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isMaximal
+ Ring.KrullDimLE.minimalPrimes_eq_setOfPred_isPrime
+ Set.coe_ofPred
+ Valuation.exists_setOfPred_restrict_le_iff
+ Walk.setOfPred_length_eq_add_one
+ Walk.setOfPred_length_eq_zero
+ Walk.setOfPred_length_eq_zero_of_ne
+ WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt
+ _root_.Irreducible.maximalIdeal_eq_setOfPred_le_v_coe
+ _root_.Irreducible.maximalIdeal_pow_eq_setOfPred_le_v_coe_pow
+ _root_.Set.Ioc_mem_ofPred_Ioc_le
+ _root_.convex_setOfPred_holderOnWith
+ _root_.convex_setOfPred_holderWith
+ addSubmonoid_closure_setOfPred_eq_monomial
+ add_closure_setOfPred_eq_single
+ ae_finite_setOfPred_mem
+ aeconst_of_dense_setOfPred_preimage_smul_ae
+ aeconst_of_dense_setOfPred_preimage_smul_eq
+ aeconst_of_dense_setOf_preimage_vadd_ae
+ aeconst_of_dense_setOf_preimage_vadd_eq
+ antitone_ofPred
+ bddAbove_setOfPred_infinite_setOfPred_apply_eq
+ bddAbove_setOfPred_k_lt_card
+ closure_inter_setOfPred_isNonloop_eq
+ closure_setOfPred_im_lt
+ closure_setOfPred_lt_im
+ closure_setOfPred_lt_re
+ closure_setOfPred_re_lt
+ codiscreteWithin_setOfPred_analyticOrderAt_eq_zero_or_top
+ codiscreteWithin_setOfPred_meromorphicOrderAt_eq_zero_or_top
+ codiscrete_setOfPred_analyticOrderAt_eq_zero_or_top
+ codiscrete_setOfPred_meromorphicOrderAt_eq_zero_or_top
+ coe_setOfPred
+ coe_span_singleton_eq_setOfPred_le_v_algebraMap
+ coe_span_singleton_eq_setOfPred_le_v_coe
+ compl_ofPred
+ compl_setOfPred_mem
+ countable_ofPred_finite_subset
+ countable_ofPred_nonempty_of_disjoint
+ countable_setOfPred_covBy_right
+ countable_setOfPred_isolated_left
+ countable_setOfPred_isolated_left_within
+ countable_setOfPred_isolated_right
+ countable_setOfPred_isolated_right_within
+ countable_setOf_covBy_left
+ decidableOfPred
+ diagSet_compl_eq_setOfPred_not_isDiag
+ diagSet_eq_setOfPred_isDiag
+ edgeSet_eq_setOfPred_exists_isLink
+ edgeSet_subset_ofPred_not_isDiag
+ eq_mem_ofPred
+ eq_setOfPred_le_sSup_and_isAtom
+ equivSetOfPred
+ exists_infinite_setOfPred_apply_eq
+ exists_isSemilinearSet_setOfPred_le
+ finite_setOfPred_absNorm_eq
+ finite_setOfPred_absNorm_le
+ finite_setOfPred_absNorm_le₀
+ finite_setOfPred_addOrderOf_eq
+ finite_setOfPred_apply_eq_iff_not_small
+ finite_setOfPred_apply_eq_k_add_one
+ finite_setOfPred_bounded
+ finite_setOfPred_isIntegral_nat_mul_and_mulHeight₁_le
+ finite_setOfPred_isMin
+ finite_setOfPred_isRestriction
+ finite_setOfPred_isRoot
+ finite_setOfPred_k_lt_card
+ finite_setOfPred_logHeight₁_le
+ finite_setOfPred_matroid
+ finite_setOfPred_mem
+ finite_setOfPred_mulHeight_nat_le
+ finite_setOfPred_mulHeight₁_le
+ finite_setOfPred_pattern_support_eq
+ finite_setOfPred_prod_infinitePlace_iSup_le
+ finite_setOfPred_setGcd_dvd_and_mem_span
+ frontier_setOfPred_im_le
+ frontier_setOfPred_im_lt
+ frontier_setOfPred_le_im
+ frontier_setOfPred_le_re
+ frontier_setOfPred_le_re_and_im_le
+ frontier_setOfPred_le_re_and_le_im
+ frontier_setOfPred_lt_im
+ frontier_setOfPred_lt_re
+ frontier_setOfPred_re_le
+ frontier_setOfPred_re_lt
+ generateFrom_setOfPred_isOpen
+ iInter_ofPred
+ iInter_setOfPred_subset
+ iUnion_ofPred
+ iUnion_smul_eq_ofPred_exists
+ iUnion_vadd_eq_setOf_exists
+ image_antitone_setOfPred_minimal
+ image_antitone_setOfPred_minimal_mem
+ image_antitone_setOf_maximal
+ image_antitone_setOf_maximal_mem
+ image_monotone_setOfPred_minimal
+ image_monotone_setOfPred_minimal_mem
+ image_monotone_setOf_maximal
+ image_monotone_setOf_maximal_mem
+ image_setOf_maximal
+ infinite_setOfPred_apply_eq_anti
+ infinite_setOfPred_apply_eq_iff_small
+ infinite_setOfPred_apply_eq_k
+ infinite_setOfPred_apply_eq_one
+ infinite_setOfPred_prime
+ infinite_setOfPred_prime_and_eq_mod
+ infinite_setOfPred_prime_and_modEq
+ infinite_setOfPred_prime_modEq_one
+ infinite_setOfPred_pseudoprimes
+ injOn_setOfPred_apply_add_one_eq_of_M_le
+ injOn_setOfPred_mem_Icc_setOfPred_lower_eq
+ instance : Algebra P.Core R
+ instance : Algebra P.Core S
+ instance : CommRing (D.subalgebra R)
+ instance : PartialOrder (MulArchimedeanClass M)
+ instance {k : ℕ} : Fintype (fiber α k) := inferInstanceAs <| Fintype (Set.ofPred _)
+ integral_lt_integral_of_ae_le_of_measure_setOfPred_lt_ne_zero
+ inter_ofPred_eq_sep
+ inter_preimage_setOfPred_minimal_eq_of_subset
+ inter_preimage_setOf_maximal_eq_of_subset
+ interior_setOfPred_eq
+ interior_setOfPred_im_le
+ interior_setOfPred_le_im
+ interior_setOfPred_le_re
+ interior_setOfPred_re_le
+ inv_ofPred
+ isClopen_setOfPred_analyticOrderAt_eq_top
+ isClopen_setOfPred_mapsTo
+ isClopen_setOfPred_meromorphicOrderAt_eq_top
+ isClopen_setOfPred_rel
+ isClosed_setOfPred_blockTriangular
+ isClosed_setOfPred_clusterPt
+ isClosed_setOfPred_concaveOn
+ isClosed_setOfPred_convexOn
+ isClosed_setOfPred_iff
+ isClosed_setOfPred_inseparable
+ isClosed_setOfPred_isCompactOperator
+ isClosed_setOfPred_lipschitzOnWith
+ isClosed_setOfPred_lipschitzWith
+ isClosed_setOfPred_map_inv
+ isClosed_setOfPred_map_mul
+ isClosed_setOfPred_map_one
+ isClosed_setOfPred_map_smul
+ isClosed_setOfPred_mapsTo
+ isClosed_setOfPred_preimage_ae_eq
+ isClosed_setOfPred_specializes
+ isClosed_setOfPred_sublevelLeft_subset
+ isClosed_setOfPred_tendsto_birkhoffAverage
+ isClosed_setOf_map_add
+ isClosed_setOf_map_neg
+ isClosed_setOf_map_zero
+ isCofinal_setOfPred_imp_lt
+ isCompact_setOfPred_finiteMeasure_eq_of_compactSpace
+ isCompact_setOfPred_finiteMeasure_le_of_compactSpace
+ isCompact_setOfPred_finiteMeasure_le_of_isCompact
+ isCompact_setOfPred_finiteMeasure_mass_eq_compl_isCompact_le
+ isCompact_setOfPred_finiteMeasure_mass_le_compl_isCompact_le
+ isCompact_setOfPred_probabilityMeasure_mass_eq_compl_isCompact_le
+ isComplete_setOfPred_eqOn
+ isConnected_setOfPred_sOppSide
+ isConnected_setOfPred_sSameSide
+ isConnected_setOfPred_sameRay
+ isConnected_setOfPred_sameRay_and_ne_zero
+ isConnected_setOfPred_wOppSide
+ isConnected_setOfPred_wSameSide
+ isLowerSet_setOfPred
+ isOpen_setOfPred_affineIndependent
+ isOpen_setOfPred_disjoint_nhds_nhds
+ isOpen_setOfPred_eventually_nhds
+ isOpen_setOfPred_eventually_nhdsWithin
+ isOpen_setOfPred_harmonicAt
+ isOpen_setOfPred_linearIndependent
+ isOpen_setOfPred_mapsTo
+ isOpen_setOfPred_mem
+ isOpen_setOfPred_mem_nhds_and_isMaxOn_norm
+ isOpen_setOfPred_nat_le_rank
+ isOpen_setOfPred_range_subset
+ isOpen_setOf_rel
+ isPreconnected_setOfPred_sOppSide
+ isPreconnected_setOfPred_sSameSide
+ isPreconnected_setOfPred_wOppSide
+ isPreconnected_setOfPred_wSameSide
+ isPrincipal_iff_exists_eq_setOfPred_valuation_le
+ isSemilinearSet_setOfPred_eq
+ isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall
+ isUpperSet_setOfPred
+ mapOfPredMaximal
+ mapOfPredMinimal
+ maximalIdeal_eq_setOfPred_le_v_algebraMap
+ maximalIdeal_pow_eq_setOfPred_le_v_algebraMap_pow
+ measurableSet_setOfPred
+ measurable_setOfPred
+ measure_setOfPred_frequently_eq_zero
+ mem_iff_mem
+ mem_ofPred
+ mem_ofPred_eq
+ mem_εClosure_of_mem_step
+ monotone_ofPred
+ neg_setOf
+ nonempty_setOfPred_infinite_setOfPred_apply_eq
+ notMem_ofPred_iff
+ not_bddAbove_setOfPred_isPrincipal
+ not_bddAbove_setOfPred_prime
+ ofPred_and
+ ofPred_bijective
+ ofPred_bot
+ ofPred_eq_eq_singleton
+ ofPred_eq_eq_singleton'
+ ofPred_exists
+ ofPred_false
+ ofPred_forall
+ ofPred_inj
+ ofPred_injective
+ ofPred_inter_eq_sep
+ ofPred_mem_eq
+ ofPred_mem_list_eq_replicate
+ ofPred_mem_list_eq_singleton_of_nodup
+ ofPred_or
+ ofPred_subset
+ ofPred_subset_ofPred
+ ofPred_subset_ofPred_of_imp
+ ofPred_top
+ ofPred_true
+ ordConnected_setOfPred_closedEBall_subset
+ ordConnected_setOfPred_eball_subset
+ polarSubmodule_eq_setOfPred
+ preimage_ofPred_eq
+ preimage_setOfPred_dist
+ schnirelmannDensity_setOfPred_Odd
+ schnirelmannDensity_setOfPred_even
+ schnirelmannDensity_setOfPred_mod_eq_one
+ schnirelmannDensity_setOfPred_modeq_one
+ schnirelmannDensity_setOfPred_prime
+ sdiff_mem_nhdsWithin
+ search
+ self_subset_setOfPred_gauge_le_one
+ sep_ofPred
+ sep_subset_ofPred
+ setOfMaximalIsoSetOfMinimal
+ setOfPred
+ setOfPredMinimalIsoSetOfPredMaximal
+ setOfPred_apply_eq_of_apply_big_of_N'_le
+ setOfPred_apply_symm_eq_image_setOfPred
+ setOfPred_dep_eq
+ setOfPred_dual_isBase_eq
+ setOfPred_gauge_le_eq
+ setOfPred_gauge_lt_eq
+ setOfPred_gauge_lt_one_eq_interior
+ setOfPred_gauge_lt_one_eq_self_of_isOpen
+ setOfPred_gauge_lt_one_subset_self
+ setOfPred_indep_eq
+ setOfPred_index_eq_univ
+ setOfPred_isClosed_eq_range_closure
+ setOfPred_isExtremePt_eq_bot
+ setOfPred_isExtremePt_isAdmissible
+ setOfPred_isMaximal_finite
+ setOfPred_isNonloop_eq
+ setOfPred_isOpen
+ setOfPred_isOpen_iSup
+ setOfPred_isOpen_injective
+ setOfPred_isOpen_sSup
+ setOfPred_isOpen_sup
+ setOfPred_isPreconnected_eq_of_ordered
+ setOfPred_isPreconnected_subset_of_ordered
+ setOfPred_isPrime_finite
+ setOfPred_isUnit_inter_mul_comm
+ setOfPred_liouvilleWith_subset_aux
+ setOfPred_liouville_eq_iInter_iUnion
+ setOfPred_liouville_eq_irrational_inter_iInter_iUnion
+ setOfPred_maximal_antichain
+ setOfPred_mem
+ setOfPred_mem_eq
+ setOfPred_mem_eq_empty_iff
+ setOfPred_mem_eq_univ_iff
+ setOfPred_mem_integer_eq_closedBall
+ setOfPred_minimal_antichain
+ setOfPred_minimal_subset
+ setOfPred_odd_degree_eq
+ setOfPred_polynomial_valuation_lt_one_and_ne_zero_nonempty
+ setOfPred_pow_dvd_eq_Icc_factorization
+ setOfPred_riemannianEDist_lt_subset_nhds
+ setOfPred_root_add_zsmul_eq_Icc_of_linearIndependent
+ setOfPred_root_add_zsmul_mem_eq_Icc
+ setOfPred_root_sub_zsmul_mem_eq_Icc
+ setOfPred_sOppSide_eq_image2
+ setOfPred_sSameSide_eq_image2
+ setOfPred_sublevelLeft_subset
+ setOfPred_subset_eq_empty_iff
+ setOfPred_subset_eq_univ_iff
+ setOfPred_wOppSide_eq_image2
+ setOfPred_wSameSide_eq_image2
+ setOf_maximal_subset
+ span_setOfPred_mem_eq_top
+ subset_ofPred
+ subsingleton_setOfPred_mem_iff_pairwise_disjoint
+ surjective_count_of_infinite_setOfPred
+ toNat_nat
+ volume_iUnion_setOfPred_liouvilleWith
+ volume_setOfPred_liouville
+ εClosure.base
+ εClosure.step
++ definition
++ dense_setOfPred_finite
++ image_setOfPred_minimal
++ isClosed_setOfPred_continuous
++ isClosed_setOfPred_totallyBounded
++ setOfPred_mem_sym2
++ toFinset_ofPred
++- toSet
++-- dense_setOf_finite
++-- image_setOf_minimal
++-- isClosed_setOf_continuous
++-- isClosed_setOf_totallyBounded
++-- setOf
++-- setOf_mem_eq
++-- setOf_mem_sym2
++-- toFinset_setOf
- Mem
- Nat.isSemilinearSet_setOf_eq
- _root_.Irreducible.maximalIdeal_eq_setOf_le_v_coe
- _root_.Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow
- _root_.Set.Ioc_mem_setOf_Ioc_le
- _root_.convex_setOf_holderOnWith
- _root_.convex_setOf_holderWith
- exists_isSemilinearSet_setOf_le
- finite_setOf_bounded
- finite_setOf_isIntegral_nat_mul_and_mulHeight₁_le
- instance : Algebra P.Core R := fast_instance% (inferInstanceAs <| Algebra P.core R)
- instance : Algebra P.Core S := fast_instance% (inferInstanceAs <| Algebra P.core S)
- instance : CommRing (D.subalgebra R) := inferInstanceAs <| CommRing (Algebra.adjoin _ _)
- instance {k : ℕ} : Fintype (fiber α k) := inferInstanceAs <| Fintype (setOf _)
- setOf_eq_eq_singleton'
- spanCarrier
-+-+ Ioo_ae_eq_Icc
-+-+ congr

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

---

Increase in strong tech debt: (relative, absolute) = (2.86, 0.74)

Current number	Change	Type (strong)
145	-1	adaptation notes
497	-1	erw
4	3	maxHeartBeats modifications
4525	-1	backward.defeqAttrib.useBackward
5619	2	backward.isDefEq.respectTransparency

No changes to weak technical debt.

Current commit 9c730e85e9
Reference commit 8ccb214159

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• chore: add missing noncomputable #41446
• chore(Data): rename setOf to Set.ofPred #41507
• refactor: notation for EventuallyEq on Set #41533
  By Dependent Issues (🤖). Happy coding!

[themathqueen]

Note that this basically takes over #39211.