Commit 2025-10-31 10:48 be6b01d8

View on Github →

feat(Finset): interaction of attach and cons (#31025) and golf the corresponding insert lemma. This lets us golf a proof by induction.

Estimated changes

Modified Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean

Modified Mathlib/Data/Finset/Image.lean

added theorem Finset.attach_cons

modified theorem Finset.attach_insert