Arctan

📁 Source: Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean

Statistics

Metric	Count
Definitions evalRealArctan, evalRealCosArctan, evalRealSinArctan, arctan, tanOrderIso, tanPartialHomeomorph	6
Theorems arccos_eq_arctan, arcsin_eq_arctan, arctan_add, arctan_add_arctan_lt_pi_div_two, arctan_add_eq_add_pi, arctan_add_eq_sub_pi, arctan_eq_arccos, arctan_eq_arcsin, arctan_eq_neg_pi_div_four, arctan_eq_of_tan_eq, arctan_eq_pi_div_four, arctan_eq_zero_iff, arctan_inj, arctan_injective, arctan_inv_2_add_arctan_inv_3, arctan_inv_of_neg, arctan_inv_of_pos, arctan_inv_sqrt_three, arctan_le_arctan, arctan_le_arctan_iff, arctan_le_zero, arctan_lt_arctan, arctan_lt_arctan_iff, arctan_lt_pi_div_two, arctan_lt_zero, arctan_mem_Ioo, arctan_mono, arctan_ne_mul_pi_div_two, arctan_neg, arctan_nonneg, arctan_one, arctan_pos, arctan_sqrt_three, arctan_strictMono, arctan_tan, arctan_zero, coe_tanPartialHomeomorph, coe_tanPartialHomeomorph_symm, continuousAt_arctan, continuousOn_tan, continuousOn_tan_Ioo, continuous_arctan, continuous_tan, cos_arctan, cos_arctan_pos, cos_sq_arctan, four_mul_arctan_inv_5_sub_arctan_inv_239, image_tan_Ioo, neg_pi_div_two_lt_arctan, range_arctan, sin_arctan, sin_arctan_eq_zero, sin_arctan_le_zero, sin_arctan_lt_zero, sin_arctan_nonneg, sin_arctan_pos, sin_arctan_strictMono, sin_sq_arctan, surjOn_tan, tan_add, tan_add', tan_arctan, tan_int_mul_pi_div_two, tan_sub, tan_sub', tan_surjective, tan_two_mul, tendsto_arctan_atBot, tendsto_arctan_atTop, two_mul_arctan, two_mul_arctan_add_pi, two_mul_arctan_inv_2_sub_arctan_inv_7, two_mul_arctan_inv_3_add_arctan_inv_7, two_mul_arctan_sub_pi	74
Total	80

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalRealArctan 📖	CompOp	—
evalRealCosArctan 📖	CompOp	—
evalRealSinArctan 📖	CompOp	—

Real

Definitions

Name	Category	Theorems
arctan 📖	CompOp	108 math math: arctan_eq_arccos, differentiable_arctan, sin_arctan, deriv_arctan, Orientation.oangle_add_left_smul_rotation_pi_div_two, Complex.ofReal_arctan, arctan_eq_arcsin, arctan_nonneg, sin_arctan_nonneg, arctan_pos, derivWithin_arctan, Orientation.oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two, EuclideanGeometry.angle_eq_arctan_of_angle_eq_pi_div_two, range_arctan, arctan_eq_zero_iff, HasDerivAt.arctan, arctan_mem_Ioo, neg_pi_div_two_lt_arctan, HasFDerivAt.arctan, ContDiff.arctan, arctan_le_arctan, two_mul_arctan_inv_2_sub_arctan_inv_7, EuclideanGeometry.oangle_right_eq_arctan_of_oangle_eq_pi_div_two, HasStrictDerivAt.arctan, sin_sq_arctan, arctan_add_arctan_lt_pi_div_two, two_mul_arctan, arctan_eq_neg_pi_div_four, InnerProductGeometry.angle_add_eq_arctan_of_inner_eq_zero, measurable_arctan, ContDiffWithinAt.arctan, arctan_neg, arctan_eq_of_tan_eq, arctan_inv_of_neg, DifferentiableWithinAt.arctan, sin_arctan_pos, deriv_arctan, Differentiable.arctan, arctan_strictMono, integral_div_sq_add_sq, arctan_injective, ContDiffAt.arctan, arctan_zero, HasStrictFDerivAt.arctan, fderiv_arctan, HasDerivWithinAt.arctan, Orientation.oangle_sub_right_smul_rotation_pi_div_two, differentiableAt_arctan, arctan_inj, arctan_inv_2_add_arctan_inv_3, arctan_one, arccos_eq_arctan, EuclideanGeometry.oangle_left_eq_arctan_of_oangle_eq_pi_div_two, continuous_arctan, arctan_inv_sqrt_three, integral_inv_sq_add_sq, ContDiffOn.arctan, Orientation.oangle_sub_left_smul_rotation_pi_div_two, Orientation.oangle_add_right_smul_rotation_pi_div_two, hasStrictDerivAt_arctan, arctan_le_arctan_iff, arctan_lt_zero, Orientation.oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two, sin_arctan_eq_zero, HasFDerivWithinAt.arctan, contDiff_arctan, tendsto_arctan_atTop, DifferentiableOn.arctan, Measurable.arctan, two_mul_arctan_sub_pi, tendsto_arctan_atBot, two_mul_arctan_add_pi, hasDerivAt_arctan', sin_arctan_strictMono, integral_one_div_one_add_sq, two_mul_arctan_inv_3_add_arctan_inv_7, arctan_inv_of_pos, arctan_lt_arctan, arctan_lt_pi_div_two, arctan_sqrt_three, arctan_le_zero, arctan_mono, Orientation.oangle_sub_left_eq_arctan_of_oangle_eq_pi_div_two, hasSum_arctan, sin_arctan_le_zero, integral_inv_one_add_sq, tan_arctan, coe_tanPartialHomeomorph_symm, InnerProductGeometry.angle_sub_eq_arctan_of_inner_eq_zero, arctan_add, arctan_eq_pi_div_four, integral_Ioi_inv_one_add_sq, hasDerivAt_arctan, arctan_add_eq_sub_pi, cos_arctan_pos, fderivWithin_arctan, integral_Iic_inv_one_add_sq, arcsin_eq_arctan, DifferentiableAt.arctan, continuousAt_arctan, cos_sq_arctan, Orientation.oangle_sub_right_eq_arctan_of_oangle_eq_pi_div_two, arctan_tan, four_mul_arctan_inv_5_sub_arctan_inv_239, arctan_lt_arctan_iff, sin_arctan_lt_zero, cos_arctan, arctan_add_eq_add_pi
tanOrderIso 📖	CompOp	—
tanPartialHomeomorph 📖	CompOp	2 math math: coe_tanPartialHomeomorph, coe_tanPartialHomeomorph_symm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arccos_eq_arctan 📖	mathematical	Real instLT instZero	arccos arctan DivInvMonoid.toDiv instDivInvMonoid sqrt instSub instOne Monoid.toNatPow instMonoid	—	arccos.eq_1 arctan_eq_of_tan_eq Nat.instAtLeastTwoHAddOfNat Nat.cast_one tan_pi_div_two_sub tan_arcsin inv_div lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_nonpos instIsOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul CancelDenoms.neg_subst Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true arcsin_le_pi_div_two Mathlib.Tactic.Linarith.sub_neg_of_lt pi_pos Mathlib.Tactic.Linarith.mul_neg arcsin_pos
arcsin_eq_arctan 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg instOne	arcsin arctan DivInvMonoid.toDiv instDivInvMonoid sqrt instSub Monoid.toNatPow instMonoid	—	Nat.cast_one arctan_eq_arcsin div_pow sq_sqrt le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Int.cast_neg Int.cast_one one_add_div Mathlib.Tactic.Linarith.lt_of_eq_of_lt sub_eq_zero_of_eq div_div sqrt_mul mul_div_cancel₀ sub_add_cancel sqrt_one div_one
arctan_add 📖	mathematical	Real instLT instMul instOne	instAdd arctan DivInvMonoid.toDiv instDivInvMonoid instSub	—	arctan_tan Nat.instAtLeastTwoHAddOfNat neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add neg_add arctan_neg arctan_add_arctan_lt_pi_div_two neg_mul_neg tan_arctan tan_add' arctan_ne_mul_pi_div_two
arctan_add_arctan_lt_pi_div_two 📖	mathematical	Real instLT instMul instOne	instAdd arctan DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat le_or_gt add_zero arctan_zero add_lt_add_of_lt_of_le IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add arctan_lt_pi_div_two OrderIso.monotone OrderIso.strictMono inv_eq_one_div lt_div_iff₀ MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing lt_tsub_iff_right AddGroup.toOrderedSub arctan_inv_of_pos
arctan_add_eq_add_pi 📖	mathematical	Real instLT instOne instMul instZero	instAdd arctan DivInvMonoid.toDiv instDivInvMonoid instSub pi	—	mul_pos_iff AddGroup.existsAddOfLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing IsStrictOrderedRing.toMulPosStrictMono IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_lt_of_covariant_le LT.lt.trans zero_lt_one instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike LT.lt.asymm arctan_add inv_lt_one_of_one_lt₀ PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE mul_inv add_comm arctan_neg sub_eq_add_neg sub_eq_iff_eq_add' sub_eq_iff_eq_add Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz arctan_inv_of_pos
arctan_add_eq_sub_pi 📖	mathematical	Real instLT instOne instMul instZero	instAdd arctan instSub DivInvMonoid.toDiv instDivInvMonoid pi	—	arctan_add_eq_add_pi neg_mul_neg neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid arctan_neg neg_add neg_neg sub_eq_add_neg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.one_mul
arctan_eq_arccos 📖	mathematical	Real instLE instZero	arctan arccos instInv sqrt instAdd instOne Monoid.toNatPow instMonoid	—	arctan_eq_arcsin arccos_eq_arcsin inv_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing sqrt_nonneg Nat.cast_one sqrt_inv sq_sqrt le_of_lt inv_pos_of_pos add_pos_of_pos_of_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE Nat.instAtLeastTwoHAddOfNat even_two_mul one_div one_sub_div ne_of_gt add_sub_cancel_left sqrt_div sqrt_sq Nat.cast_zero
arctan_eq_arcsin 📖	mathematical	—	arctan arcsin Real DivInvMonoid.toDiv instDivInvMonoid sqrt instAdd instOne Monoid.toNatPow instMonoid	—	arcsin_eq_of_sin_eq sin_arctan Set.mem_Icc_of_Ioo Nat.instAtLeastTwoHAddOfNat arctan_mem_Ioo
arctan_eq_neg_pi_div_four 📖	mathematical	—	arctan Real instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	—	arctan_injective Nat.instAtLeastTwoHAddOfNat arctan_neg arctan_one
arctan_eq_of_tan_eq 📖	mathematical	tan Real Set Set.instMembership Set.Ioo instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	arctan	—	Nat.instAtLeastTwoHAddOfNat injOn_tan arctan_mem_Ioo tan_arctan
arctan_eq_pi_div_four 📖	mathematical	—	arctan Real DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	—	arctan_injective Nat.instAtLeastTwoHAddOfNat arctan_one
arctan_eq_zero_iff 📖	mathematical	—	arctan Real instZero	—	arctan_zero arctan_injective
arctan_inj 📖	mathematical	—	arctan	—	arctan_injective
arctan_injective 📖	mathematical	—	Real arctan	—	StrictMono.injective arctan_strictMono
arctan_inv_2_add_arctan_inv_3 📖	mathematical	—	Real instAdd arctan instInv instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid pi	—	Nat.instAtLeastTwoHAddOfNat arctan_add Mathlib.Meta.NormNum.isNNRat_lt_true instIsStrictOrderedRing instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Nat.cast_one Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_add Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.IsNNRat.to_isRat arctan_one
arctan_inv_of_neg 📖	mathematical	Real instLT instZero	arctan instInv instSub instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat arctan_inv_of_pos neg_pos IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid neg_neg arctan_neg neg_sub' neg_eq_iff_eq_neg inv_neg
arctan_inv_of_pos 📖	mathematical	Real instLT instZero	arctan instInv instSub DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat arctan_tan IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add add_halves CharZero.NeZero.two RCLike.charZero_rclike LT.lt.trans arctan_lt_pi_div_two half_lt_self_iff PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing pi_pos sub_lt_self_iff arctan_zero OrderIso.strictMono tan_pi_div_two_sub tan_arctan
arctan_inv_sqrt_three 📖	mathematical	—	arctan Real instInv sqrt instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid pi	—	Nat.instAtLeastTwoHAddOfNat inv_eq_one_div tan_pi_div_six arctan_tan Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.cons_pos instZeroLEOneClass pi_pos zero_lt_one NeZero.one GroupWithZero.toNontrivial Mathlib.Meta.NormNum.isInt_lt_true Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike
arctan_le_arctan 📖	mathematical	Real instLE	arctan	—	StrictMono.monotone arctan_strictMono
arctan_le_arctan_iff 📖	mathematical	—	Real instLE arctan	—	StrictMono.le_iff_le arctan_strictMono
arctan_le_zero 📖	mathematical	—	Real instLE arctan instZero	—	arctan_zero arctan_le_arctan_iff
arctan_lt_arctan 📖	mathematical	Real instLT	arctan	—	arctan_strictMono
arctan_lt_arctan_iff 📖	mathematical	—	Real instLT arctan	—	StrictMono.lt_iff_lt arctan_strictMono
arctan_lt_pi_div_two 📖	mathematical	—	Real instLT arctan DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat arctan_mem_Ioo
arctan_lt_zero 📖	mathematical	—	Real instLT arctan instZero	—	arctan_zero arctan_lt_arctan_iff
arctan_mem_Ioo 📖	mathematical	—	Real Set Set.instMembership Set.Ioo instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arctan	—	Subtype.coe_prop Nat.instAtLeastTwoHAddOfNat
arctan_mono 📖	mathematical	—	Monotone Real instPreorder arctan	—	StrictMono.monotone arctan_strictMono
arctan_ne_mul_pi_div_two 📖	—	—	—	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Push.not_forall_eq arctan_mem_Ioo Nat.cast_one Int.cast_ofNat Int.cast_one IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike mul_lt_mul_iff_left₀ IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pi_pos Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo mul_div_assoc one_mul neg_eq_neg_one_mul
arctan_neg 📖	mathematical	—	arctan Real instNeg	—	arctan_eq_arcsin Even.neg_pow Nat.instAtLeastTwoHAddOfNat neg_div arcsin_neg
arctan_nonneg 📖	mathematical	—	Real instLE instZero arctan	—	arctan_zero arctan_le_arctan_iff
arctan_one 📖	mathematical	—	arctan Real instOne DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	arctan_eq_of_tan_eq Nat.instAtLeastTwoHAddOfNat tan_pi_div_four lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg instIsStrictOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_mul CancelDenoms.neg_subst Mathlib.Tactic.Linarith.mul_nonpos instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt pi_pos
arctan_pos 📖	mathematical	—	Real instLT instZero arctan	—	arctan_zero arctan_lt_arctan_iff
arctan_sqrt_three 📖	mathematical	—	arctan sqrt Real instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid pi	—	Nat.instAtLeastTwoHAddOfNat tan_pi_div_three arctan_tan Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ div_one Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg LT.lt.ne' Mathlib.Meta.Positivity.pos_of_isNat instIsOrderedRing instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul mul_neg Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.cons_pos instZeroLEOneClass pi_pos zero_lt_one NeZero.one GroupWithZero.toNontrivial Mathlib.Meta.NormNum.isInt_lt_true Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike
arctan_strictMono 📖	mathematical	—	StrictMono Real instPreorder arctan	—	OrderIso.strictMono Nat.instAtLeastTwoHAddOfNat
arctan_tan 📖	mathematical	Real instLT instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	arctan tan	—	Nat.instAtLeastTwoHAddOfNat OrderIso.symm_apply_apply
arctan_zero 📖	mathematical	—	arctan Real instZero	—	arctan_eq_arcsin zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat add_zero sqrt_one div_one arcsin_zero
coe_tanPartialHomeomorph 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace tanPartialHomeomorph tan	—	—
coe_tanPartialHomeomorph_symm 📖	mathematical	—	OpenPartialHomeomorph.toFun' Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace OpenPartialHomeomorph.symm tanPartialHomeomorph arctan	—	—
continuousAt_arctan 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arctan	—	Continuous.continuousAt continuous_arctan
continuousOn_tan 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace tan setOf cos instZero	—	ContinuousOn.div IsTopologicalDivisionRing.toContinuousInv₀ instIsTopologicalDivisionRingReal IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring instIsTopologicalRingReal continuousOn_sin continuousOn_cos tan_eq_sin_div_cos
continuousOn_tan_Ioo 📖	mathematical	—	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace tan Set.Ioo instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	ContinuousOn.mono Nat.instAtLeastTwoHAddOfNat continuousOn_tan cos_eq_zero_iff le_or_gt lt_iff_not_ge one_mul mul_div_assoc mul_le_mul_iff_left₀ IsOrderedRing.toMulPosMono instIsOrderedRing MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono instIsStrictOrderedRing half_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono pi_pos covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le instNontrivial instZeroLEOneClass neg_mul_eq_neg_mul le_neg_iff_add_nonpos_right Int.instAddLeftMono le_sub_iff_add_le mul_comm le_div_iff₀ MulPosReflectLE.toMulPosReflectLT zero_lt_two NeZero.charZero_one RCLike.charZero_rclike Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.IsRat.to_isInt Mathlib.Meta.NormNum.isRat_div Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isRat_mul Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.instAtLeastTwo
continuous_arctan 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arctan	—	Continuous.comp continuous_subtype_val Homeomorph.continuous_invFun Nat.instAtLeastTwoHAddOfNat orderTopology_of_ordConnected instOrderTopologyReal Set.ordConnected_Ioo
continuous_tan 📖	mathematical	—	Continuous Set.Elem Real setOf cos instZero instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace tan	—	continuousOn_iff_continuous_restrict continuousOn_tan
cos_arctan 📖	mathematical	—	cos arctan Real DivInvMonoid.toDiv instDivInvMonoid instOne sqrt instAdd Monoid.toNatPow instMonoid	—	one_div inv_sqrt_one_add_tan_sq cos_arctan_pos tan_arctan
cos_arctan_pos 📖	mathematical	—	Real instLT instZero cos arctan	—	cos_pos_of_mem_Ioo arctan_mem_Ioo
cos_sq_arctan 📖	mathematical	—	Real Monoid.toNatPow instMonoid cos arctan DivInvMonoid.toDiv instDivInvMonoid instOne instAdd	—	one_div inv_one_add_tan_sq LT.lt.ne' cos_arctan_pos tan_arctan
four_mul_arctan_inv_5_sub_arctan_inv_239 📖	mathematical	—	Real instSub instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arctan instInv DivInvMonoid.toDiv instDivInvMonoid pi	—	Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw two_mul_arctan Mathlib.Meta.NormNum.isRat_lt_true instIsStrictOrderedRing DivisionRing.toNontrivial Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Nat.cast_one Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 arctan_one sub_eq_iff_eq_add arctan_add Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_add
image_tan_Ioo 📖	mathematical	—	Set.image Real tan Set.Ioo instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Set.univ	—	Nat.instAtLeastTwoHAddOfNat Set.univ_subset_iff surjOn_tan
neg_pi_div_two_lt_arctan 📖	mathematical	—	Real instLT instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arctan	—	Nat.instAtLeastTwoHAddOfNat arctan_mem_Ioo
range_arctan 📖	mathematical	—	Set.range Real arctan Set.Ioo instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Function.Surjective.range_comp EquivLike.surjective Subtype.range_coe
sin_arctan 📖	mathematical	—	sin arctan Real DivInvMonoid.toDiv instDivInvMonoid sqrt instAdd instOne Monoid.toNatPow instMonoid	—	tan_div_sqrt_one_add_tan_sq cos_arctan_pos tan_arctan
sin_arctan_eq_zero 📖	mathematical	—	sin arctan Real instZero	—	StrictMono.injective sin_arctan_strictMono arctan_zero sin_zero
sin_arctan_le_zero 📖	mathematical	—	Real instLE sin arctan instZero	—	arctan_zero sin_zero StrictMono.le_iff_le sin_arctan_strictMono
sin_arctan_lt_zero 📖	mathematical	—	Real instLT sin arctan instZero	—	arctan_zero sin_zero StrictMono.lt_iff_lt sin_arctan_strictMono
sin_arctan_nonneg 📖	mathematical	—	Real instLE instZero sin arctan	—	arctan_zero sin_zero StrictMono.le_iff_le sin_arctan_strictMono
sin_arctan_pos 📖	mathematical	—	Real instLT instZero sin arctan	—	arctan_zero sin_zero StrictMono.lt_iff_lt sin_arctan_strictMono
sin_arctan_strictMono 📖	mathematical	—	StrictMono Real instPreorder sin arctan	—	strictMonoOn_sin Set.Ioo_subset_Icc_self Nat.instAtLeastTwoHAddOfNat arctan_mem_Ioo arctan_strictMono
sin_sq_arctan 📖	mathematical	—	Real Monoid.toNatPow instMonoid sin arctan DivInvMonoid.toDiv instDivInvMonoid instAdd instOne	—	tan_sq_div_one_add_tan_sq LT.lt.ne' cos_arctan_pos tan_arctan
surjOn_tan 📖	mathematical	—	Set.SurjOn Real tan Set.Ioo instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Set.univ	—	Nat.instAtLeastTwoHAddOfNat neg_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid pi_div_two_pos ContinuousOn.surjOn_of_tendsto instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing HasSolidNorm.orderClosedTopology instHasSolidNormReal Set.ordConnected_Ioo Set.nonempty_Ioo continuousOn_tan_Ioo tendsto_comp_coe_Ioo_atBot Order.IsPredPrelimit.of_dense tendsto_tan_neg_pi_div_two tendsto_comp_coe_Ioo_atTop Order.IsSuccPrelimit.of_dense tendsto_tan_pi_div_two
tan_add 📖	mathematical	Real DivInvMonoid.toDiv instDivInvMonoid instMul instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast instOne pi	tan instSub	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_tan Complex.ofReal_add Complex.ofReal_div Complex.ofReal_sub Complex.ofReal_mul Complex.tan_add Nat.cast_one Int.cast_ofNat Int.cast_one Int.cast_add Int.cast_mul
tan_add' 📖	mathematical	—	tan Real instAdd DivInvMonoid.toDiv instDivInvMonoid instSub instOne instMul	—	Nat.instAtLeastTwoHAddOfNat tan_add
tan_arctan 📖	mathematical	—	tan arctan	—	OrderIso.apply_symm_apply Nat.instAtLeastTwoHAddOfNat
tan_int_mul_pi_div_two 📖	mathematical	—	tan Real DivInvMonoid.toDiv instDivInvMonoid instMul instIntCast pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instZero	—	Nat.instAtLeastTwoHAddOfNat tan_eq_zero_iff
tan_sub 📖	mathematical	Real DivInvMonoid.toDiv instDivInvMonoid instMul instAdd instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instIntCast instOne pi	tan instSub	—	Nat.instAtLeastTwoHAddOfNat Complex.ofReal_tan Complex.ofReal_sub Complex.ofReal_div Complex.ofReal_add Complex.ofReal_mul Complex.tan_sub Nat.cast_one Int.cast_ofNat Int.cast_one Int.cast_add Int.cast_mul
tan_sub' 📖	mathematical	—	tan Real instSub DivInvMonoid.toDiv instDivInvMonoid instAdd instOne instMul	—	Nat.instAtLeastTwoHAddOfNat tan_sub
tan_surjective 📖	mathematical	—	Real tan	—	Set.SurjOn.subset_range Nat.instAtLeastTwoHAddOfNat surjOn_tan
tan_two_mul 📖	mathematical	—	tan Real instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat DivInvMonoid.toDiv instDivInvMonoid instSub instOne Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat Complex.tan_two_mul Nat.cast_one
tendsto_arctan_atBot 📖	mathematical	—	Filter.Tendsto Real arctan Filter.atBot instPreorder nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Set.Ioi	—	tendsto_Ioo_atBot instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing OrderIso.tendsto_atBot Nat.instAtLeastTwoHAddOfNat
tendsto_arctan_atTop 📖	mathematical	—	Filter.Tendsto Real arctan Filter.atTop instPreorder nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat Set.Iio	—	tendsto_Ioo_atTop instOrderTopologyReal LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing OrderIso.tendsto_atTop Nat.instAtLeastTwoHAddOfNat
two_mul_arctan 📖	mathematical	Real instLT instNeg instOne	instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arctan DivInvMonoid.toDiv instDivInvMonoid instSub Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat two_mul arctan_add lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_le_of_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le instIsOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero
two_mul_arctan_add_pi 📖	mathematical	Real instLT instOne	instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arctan instAdd DivInvMonoid.toDiv instDivInvMonoid instSub Monoid.toNatPow instMonoid pi	—	Nat.instAtLeastTwoHAddOfNat two_mul arctan_add_eq_add_pi lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Nat.cast_one Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Mathlib.Tactic.Ring.neg_congr neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero
two_mul_arctan_inv_2_sub_arctan_inv_7 📖	mathematical	—	Real instSub instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arctan instInv DivInvMonoid.toDiv instDivInvMonoid pi	—	Nat.instAtLeastTwoHAddOfNat two_mul_arctan Mathlib.Meta.NormNum.isRat_lt_true instIsStrictOrderedRing DivisionRing.toNontrivial Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero arctan_one sub_eq_iff_eq_add arctan_add Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.to_eq Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.isNNRat_add
two_mul_arctan_inv_3_add_arctan_inv_7 📖	mathematical	—	Real instAdd instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arctan instInv DivInvMonoid.toDiv instDivInvMonoid pi	—	Nat.instAtLeastTwoHAddOfNat two_mul_arctan Mathlib.Meta.NormNum.isRat_lt_true instIsStrictOrderedRing DivisionRing.toNontrivial Mathlib.Meta.NormNum.IsInt.to_isRat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Meta.NormNum.IsNNRat.to_isRat Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.isNNRat_lt_true instNontrivialOfCharZero IsStrictOrderedRing.toCharZero arctan_add Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsRat.to_isNNRat Mathlib.Meta.NormNum.isRat_sub Mathlib.Meta.NormNum.isNNRat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_add arctan_one
two_mul_arctan_sub_pi 📖	mathematical	Real instLT instNeg instOne	instMul instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arctan instSub DivInvMonoid.toDiv instDivInvMonoid Monoid.toNatPow instMonoid pi	—	Nat.instAtLeastTwoHAddOfNat two_mul arctan_add_eq_sub_pi lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.neg_congr Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Linarith.add_neg instIsStrictOrderedRing Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_pos_of_neg_of_neg AddGroup.existsAddOfLE IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le neg_neg_of_pos Mathlib.Tactic.Linarith.zero_lt_one Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.atom_pf' Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero

---

← Back to Index