Commit 2025-07-31 14:34 e75bdf0e

View on Github →

feat(Arctan): add more simp lemmas (#27719) Also add some positivity extensions.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

added def Mathlib.Meta.Positivity.evalRealArctan

added def Mathlib.Meta.Positivity.evalRealCosArctan

added def Mathlib.Meta.Positivity.evalRealSinArctan

modified theorem Real.arccos_eq_arctan

modified theorem Real.arcsin_eq_arctan

modified theorem Real.arctan_add

modified theorem Real.arctan_add_arctan_lt_pi_div_two

modified theorem Real.arctan_add_eq_add_pi

modified theorem Real.arctan_add_eq_sub_pi

modified theorem Real.arctan_eq_arccos

added theorem Real.arctan_eq_neg_pi_div_four

modified theorem Real.arctan_eq_of_tan_eq

added theorem Real.arctan_eq_pi_div_four

modified theorem Real.arctan_eq_zero_iff

added theorem Real.arctan_inj

modified theorem Real.arctan_inv_of_neg

modified theorem Real.arctan_inv_of_pos

modified theorem Real.arctan_le_arctan

added theorem Real.arctan_le_arctan_iff

added theorem Real.arctan_le_zero

modified theorem Real.arctan_lt_arctan

added theorem Real.arctan_lt_arctan_iff

added theorem Real.arctan_lt_zero

added theorem Real.arctan_mono

modified theorem Real.arctan_ne_mul_pi_div_two

added theorem Real.arctan_nonneg

added theorem Real.arctan_pos

modified theorem Real.arctan_tan

modified theorem Real.continuousAt_arctan

added theorem Real.sin_arctan_eq_zero

added theorem Real.sin_arctan_le_zero

added theorem Real.sin_arctan_lt_zero

added theorem Real.sin_arctan_nonneg

added theorem Real.sin_arctan_pos

added theorem Real.sin_arctan_strictMono

modified theorem Real.tan_add'

modified theorem Real.tan_add

modified theorem Real.tan_two_mul

modified theorem Real.two_mul_arctan

modified theorem Real.two_mul_arctan_add_pi

modified theorem Real.two_mul_arctan_sub_pi

Modified MathlibTest/positivity.lean