Commit 2024-09-24 00:42 87edf3cd

View on Github →

chore(Data/Finset): fix aesop finsetNonempty set (#16927) All of these examples used safe apply for a rewrite lemma, and thus weren't actually used by aesop for finsetNonempty (and thus positivity).

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

Modified Mathlib/Data/Finset/Basic.lean

Modified Mathlib/Data/Finset/Image.lean

Modified Mathlib/Data/Finset/NAry.lean

Modified Mathlib/Data/Finset/Pi.lean

Modified Mathlib/Data/Finset/Powerset.lean

Modified Mathlib/Data/Finset/Prod.lean

Modified Mathlib/Data/Finset/Sigma.lean

Modified Mathlib/Data/Finset/Sups.lean

Modified Mathlib/Data/Finset/Sym.lean

Modified Mathlib/Data/Fintype/Basic.lean

Modified Mathlib/Data/Fintype/Pi.lean

Modified Mathlib/Order/Interval/Finset/Basic.lean

modified theorem Finset.nonempty_Iic

modified theorem Finset.nonempty_Iio