MathFunctions helper lemmas

TorchLean sometimes writes scalar specs using MathFunctions.* (to keep the spec polymorphic over α) but then specializes to ℝ in proofs.

For ℝ, the MathFunctions methods are definitionally equal to their Real.* counterparts. We keep named lemmas here so proof scripts can rewrite uniformly without repeating the same rfl helpers across modules.

theorem Proofs.mathfunc_exp_eq_rexp (x : ℝ) : MathFunctions.exp x = Real.exp x

MathFunctions.exp is definitional equal to Real.exp for ℝ.

theorem Proofs.mathfunc_sinh_eq_rsinh (x : ℝ) : MathFunctions.sinh x = Real.sinh x

MathFunctions.sinh is definitional equal to Real.sinh for ℝ.

theorem Proofs.mathfunc_cosh_eq_rcosh (x : ℝ) : MathFunctions.cosh x = Real.cosh x

MathFunctions.cosh is definitional equal to Real.cosh for ℝ.