Commit 2024-10-29 07:44 fe4820c9

View on Github →

feat(Tactic): add finiteness tactic (#18034) Upstreamed from the PFR project. From PFR, Carleson, GibbsMeasure

Estimated changes

Modified Archive/Wiedijk100Theorems/BirthdayProblem.lean

Modified Mathlib.lean

Modified Mathlib/Data/ENNReal/Basic.lean

modified theorem ENNReal.coe_ne_top

modified theorem ENNReal.natCast_ne_top

added theorem ENNReal.ofNat_lt_top

added theorem ENNReal.ofNat_ne_top

modified theorem ENNReal.ofReal_ne_top

deleted theorem ENNReal.one_ne_top

modified theorem ENNReal.two_lt_top

modified theorem ENNReal.two_ne_top

deleted theorem ENNReal.zero_ne_top

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/ENNReal/Operations.lean

Modified Mathlib/MeasureTheory/Measure/Typeclasses.lean

Modified Mathlib/Order/BoundedOrder.lean

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Finiteness.lean

Created Mathlib/Tactic/Finiteness/Attr.lean

Modified scripts/noshake.json

Created test/finiteness.lean