Commit 2026-02-22 22:01 44faade3

View on Github →

feat(Tactic): linarith and rify for NNReal (#35155)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/NNReal/Basic.lean

added theorem NNReal.toReal_eq

added theorem NNReal.toReal_le

added theorem NNReal.toReal_lt

added theorem NNReal.toReal_ne

Modified Mathlib/Tactic.lean

Created Mathlib/Tactic/Linarith/NNRealPreprocessor.lean

added def Mathlib.Tactic.Linarith.isNNRealtoReal

added def Mathlib.Tactic.Linarith.mk_toReal_nonneg_prf

Modified Mathlib/Tactic/Linarith/Preprocessing.lean

added def Mathlib.Tactic.Linarith.nnrealToReal

Modified Mathlib/Tactic/Rify.lean

added def Mathlib.Tactic.Rify.mkRifyContext

added def Mathlib.Tactic.Rify.rifyProof

Renamed MathlibTest/linarith.lean to MathlibTest/Linarith/Basic.lean

Created MathlibTest/Linarith/NNReal.lean

Modified MathlibTest/Rify.lean