evalRealSinArctan — Mathlib

Lean4
/-- Extension for `Real.sin (Real.arctan _)`. -/
@[positivity Real.sin (Real.arctan _)]
def evalRealSinArctan : PositivityExt where
  eval {u α} z p
    e := do
    match u, α, e with
    | 0, ~q(ℝ), ~q(Real.sin (Real.arctan $a)) =>
      assumeInstancesCommute
      match ← core z p a with
      | .positive pa =>
        return .positive q(Real.sin_arctan_pos.mpr $pa)
      | .nonnegative na =>
        return .nonnegative q(Real.sin_arctan_nonneg.mpr $na)
      | .nonzero na =>
        return .nonzero q(mt Real.sin_arctan_eq_zero.mp $na)
      | .none =>
        return .none
    | _ =>
      throwError"not Real.sin (Real.arctan _)"
Похожие утверждения