Commit 2026-01-21 17:08 ee8bc949

View on Github →

feat(Data/Set/Finite): make simp more powerful (#33911) From ProofBench

Estimated changes

Modified Archive/Examples/Kuratowski.lean

Modified Mathlib/Data/Finite/Defs.lean

added theorem Set.Infinite.not_finite

Modified Mathlib/Data/Set/Finite/Basic.lean

modified theorem Set.Finite.diff

modified theorem Set.finite_univ