Commit 2025-03-12 12:49 0c839fe2

View on Github →

chore(Data/Finset): process porting notes (#22839) Some subtle elaboration differences mean some of the original mathlib3 proofs didn't work, but we can usually aesop them.

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/Defs.lean

Modified Mathlib/Data/Finset/Disjoint.lean

Modified Mathlib/Data/Finset/Empty.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/Insert.lean

Modified Mathlib/Data/Finset/Lattice/Basic.lean

Modified Mathlib/Data/Finset/Lattice/Pi.lean

Modified Mathlib/Data/Finset/Max.lean

Modified Mathlib/Data/Finset/PImage.lean

Modified Mathlib/Data/Finset/PiInduction.lean

Modified Mathlib/Data/Finset/Powerset.lean

Modified Mathlib/Data/Finset/Preimage.lean

added theorem Finset.preimage_compl'

Modified Mathlib/Data/Finset/Slice.lean

Modified Mathlib/Data/Finset/Sups.lean

Modified Mathlib/Data/Finset/Sym.lean

Modified Mathlib/Data/Finset/Union.lean

modified theorem Finset.biUnion_congr

modified theorem Finset.biUnion_insert

Modified Mathlib/Data/Sym/Basic.lean