Commit 2026-09-25 10:58 a61b94c2

View on Github →

chore(Analysis): use autoParam for positivity goals (#44063) The tactic fun_prop can now automatically discharge auto parameters. We add autoparams for a few positivity goals so that they can be proved by fun_prop.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean

modified theorem NNReal.continuous_nnrpow_const

Modified Mathlib/Analysis/SpecialFunctions/Pow/Continuity.lean

modified theorem NNReal.continuous_rpow_const

modified theorem Real.continuousAt_const_rpow'

modified theorem Real.continuousAt_const_rpow

modified theorem Real.continuous_const_rpow

modified theorem Real.continuous_rpow_const

Modified Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean