Commit 2026-02-25 08:52 6dc81b82

View on Github →

chore(*): reduce defeq abuse around Set (#35752)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/Combinatorics/Quiver/ConnectedComponent.lean

Modified Mathlib/Combinatorics/SimpleGraph/Copy.lean

Modified Mathlib/Data/Nat/Order/Lemmas.lean

Modified Mathlib/Data/PFun.lean

modified def PFun.fn

Modified Mathlib/Data/PNat/Basic.lean

Modified Mathlib/Data/Set/Basic.lean

Modified Mathlib/Data/Set/CoeSort.lean

modified theorem Set.elem_mem

Modified Mathlib/Data/Set/Function.lean

modified theorem Set.injOn_subtype_val

Modified Mathlib/Data/Set/Image.lean

added theorem Set.image_diff_subset

modified theorem Set.preimage_injective

modified theorem Set.preimage_surjective

Modified Mathlib/Data/Vector/MapLemmas.lean

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Order/BooleanAlgebra/Set.lean

Modified Mathlib/Order/Minimal.lean

Modified Mathlib/Order/Monotone/Defs.lean

modified theorem Subtype.mono_coe

modified theorem Subtype.strictMono_coe

Modified Mathlib/Order/PiLex.lean

Modified Mathlib/Order/WellFounded.lean