[Merged by Bors] - refactor(SetTheory/ZFC): deduplicate coercion to sets by YaelDillies · Pull Request #31287 · leanprover-community/mathlib4

YaelDillies · 2025-11-05T14:55:01Z

Currently, we have both ZFSet.toSet and SetLike.coe to turn a ZFSet into a Set ZFSet. This is bad for simp normal form. This PR removes the first spelling in favor of the second one.

Currently, we have both `ZFSet.toSet` and `SetLike.coe` to turn a `ZFSet` into a `Set ZFSet`. This is bad for simp normal form. This PR removes the first spelling in favor of the second one.

github-actions · 2025-11-05T14:56:07Z

PR summary 7df0b99484

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ coeEquiv
+ coe_empty
+ coe_iUnion
+ coe_image
+ coe_insert
+ coe_inter
+ coe_pair
+ coe_range
+ coe_sInter
+ coe_sUnion
+ coe_sdiff
+ coe_sep
+ coe_singleton
+ coe_subset_coe
+ coe_union
+ instance : HasSubset ZFSet := ⟨ZFSet.Subset⟩
+ instance : SetLike ZFSet.{u} ZFSet.{u}
+ mem_sdiff
+ nonempty_coe
+ notMem_singleton
+ sep_mem
+ sep_notMem
+ sep_subset
+ small_coe
- hasSubset
- instance : SetLike ZFSet ZFSet

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/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/SetTheory/ZFC/Basic.lean

staroperator · 2025-11-05T20:00:42Z

Mathlib/SetTheory/ZFC/Basic.lean

+  Quotient.inductionOn₂ x y fun _ _ h => Quotient.sound (Mem.ext fun w => h ⟦w⟧)
+
+instance : SetLike ZFSet.{u} ZFSet.{u} where
+  coe x := {y | y ∈ x}


Since this file used { x | p } only, could you please follow this style?

Suggested change

coe x := {y | y ∈ x}

coe x := { y | y ∈ x }

This looks like remnants from the port, since mathport was wrongly inserting the spaces. I'll keep it like that

So {y | y ∈ x} is actually preferred in Mathlib?

OK, resolved

staroperator

Looks good! Maybe beyond this PR, what should we do with PSet.toSet after deprecating ZFSet.toSet (note that PSet is not SetLike)?

YaelDillies · 2025-11-06T19:48:12Z

We keep it, most likely

jcommelin · 2025-11-21T10:47:34Z

Thanks 🎉

bors merge

Currently, we have both `ZFSet.toSet` and `SetLike.coe` to turn a `ZFSet` into a `Set ZFSet`. This is bad for simp normal form. This PR removes the first spelling in favor of the second one.

mathlib-bors · 2025-11-21T11:14:41Z

Build failed (retrying...):

Post-Build Step

Currently, we have both `ZFSet.toSet` and `SetLike.coe` to turn a `ZFSet` into a `Set ZFSet`. This is bad for simp normal form. This PR removes the first spelling in favor of the second one.

mathlib-bors · 2025-11-21T12:00:13Z

Pull request successfully merged into master.

Build succeeded:

refactor(SetTheory/ZFC): deduplicate coercion to sets

8b1a259

Currently, we have both `ZFSet.toSet` and `SetLike.coe` to turn a `ZFSet` into a `Set ZFSet`. This is bad for simp normal form. This PR removes the first spelling in favor of the second one.

github-actions bot added the t-set-theory Set theory label Nov 5, 2025

YaelDillies mentioned this pull request Nov 5, 2025

[Merged by Bors] - feat(SetTheory/ZFC): add ZFSet.card #29365

Closed

2 tasks

YaelDillies added 3 commits November 5, 2025 15:05

fix

a6328c0

fix

5fdf989

fix

5d50e53