refactor: unify `Set.mem_ofPred_eq` into `Set.mem_ofPred` by Parcly-Taxel · Pull Request #42692 · leanprover-community/mathlib4

Parcly-Taxel · 2026-08-12T15:28:23Z

Before:

@[simp, mfld_simps, push]
theorem mem_ofPred_eq {x : α} {p : α → Prop} : (x ∈ {y | p y}) = p x := rfl

theorem mem_ofPred {a : α} {p : α → Prop} : a ∈ { x | p x } ↔ p a := Iff.rfl

After:

@[simp, mfld_simps, push]
theorem mem_ofPred {x : α} {p : α → Prop} : (x ∈ {y | p y}) = p x := rfl

@[deprecated (since := "2026-08-12")] alias mem_ofPred_eq := mem_ofPred

Note that the lemma with iff is unusable by dsimp.

awaiting-zulip: #mathlib4 > Set.mem_setOf_eq @ 💬

github-actions · 2026-08-12T15:29:53Z

PR summary c57e5df72a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

+ _root_.Membership.mem.out

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)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit c57e5df).

+0 new declarations
−0 removed declarations

No declaration differences.

No changes to strong technical debt.
No changes to weak technical debt.

Current commit c57e5df72a
Reference commit 8fe7ce475b

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.py 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).

eric-wieser · 2026-08-13T13:19:46Z

Can you make clear in the description what the statements before and after this change are? The diff is full of replacements that obscure that.

Parcly-Taxel · 2026-08-13T15:23:40Z

Can you make clear in the description what the statements before and after this change are? The diff is full of replacements that obscure that.

Done.

eric-wieser · 2026-08-13T16:14:30Z

Done.

Could you make it a little clearer, and repeat the exact statement (and deprecations) of the lemmas before and after this change?

A Zulip poll suggested removing Set.mem_ofPred_eq.

I don't think the zulip poll was voting to remove the Iff version; or equivalently, the vote did not makes clear that the names were being swapped around.

Parcly-Taxel · 2026-08-14T02:50:08Z

I don't think the zulip poll was voting to remove the Iff version; or equivalently, the vote did not makes clear that the names were being swapped around.

I made another poll to see what the name of the remaining lemma should be.

mathlib-merge-conflicts · 2026-08-14T22:55:56Z