evalSinh — Mathlib

Lean4
/-- Extension for the `positivity` tactic: `Real.sinh` is positive/nonnegative/nonzero if its input
is. -/
@[positivity Real.sinh _]
def evalSinh : PositivityExt where
  eval {u α} _ _
    e := do
    let zα : Q(Zero ℝ) := q(inferInstance)
    let pα : Q(PartialOrder ℝ) := q(inferInstance)
    match u, α, e with
    | 0, ~q(ℝ), ~q(Real.sinh $a) =>
      assumeInstancesCommute
      match ← core zα pα a with
      | .positive pa =>
        return .positive q(sinh_pos_of_pos $pa)
      | .nonnegative pa =>
        return .nonnegative q(sinh_nonneg_of_nonneg $pa)
      | .nonzero pa =>
        return .nonzero q(sinh_ne_zero_of_ne_zero $pa)
      | _ =>
        return .none
    | _, _, _ =>
      throwError"not Real.sinh"
Похожие утверждения