Inverse

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

Statistics

Metric	Count
Definitions arccos, arcsin, cosPartialEquiv, cosPartialHomeomorph, sinPartialEquiv, sinPartialHomeomorph	6
Theorems arccos, arcsin, arccos, arcsin, arccos, arcsin, arccos, arcsin, arccos, arccos_nhdsGE, arccos_nhdsLE, arcsin, arcsin_nhdsGE, arcsin_nhdsLE, antitone_arccos, arccos_cos, arccos_eq_arcsin, arccos_eq_of_eq_cos, arccos_eq_pi, arccos_eq_pi_div_two, arccos_eq_pi_div_two_sub_arcsin, arccos_eq_zero, arccos_image_Icc, arccos_inj, arccos_injOn, arccos_le_arccos, arccos_le_pi, arccos_le_pi_div_four, arccos_le_pi_div_two, arccos_lt_arccos, arccos_lt_pi, arccos_lt_pi_div_two, arccos_neg, arccos_neg_one, arccos_nonneg, arccos_of_le_neg_one, arccos_of_one_le, arccos_one, arccos_pos, arccos_zero, arcsin_eq_arccos, arcsin_eq_iff_eq_sin, arcsin_eq_neg_pi_div_two, arcsin_eq_of_sin_eq, arcsin_eq_pi_div_two, arcsin_eq_pi_div_two_sub_arccos, arcsin_eq_zero_iff, arcsin_image_Icc, arcsin_inj, arcsin_le_arcsin, arcsin_le_iff_le_sin, arcsin_le_iff_le_sin', arcsin_le_neg_pi_div_two, arcsin_le_pi_div_two, arcsin_lt_arcsin, arcsin_lt_iff_lt_sin, arcsin_lt_iff_lt_sin', arcsin_lt_pi_div_two, arcsin_lt_zero, arcsin_mem_Icc, arcsin_neg, arcsin_neg_one, arcsin_nonneg, arcsin_nonpos, arcsin_of_le_neg_one, arcsin_of_one_le, arcsin_one, arcsin_pos, arcsin_projIcc, arcsin_sin, arcsin_sin', arcsin_zero, continuousAt_arcsin, continuous_arccos, continuous_arcsin, cosPartialEquiv_apply, cosPartialEquiv_source, cosPartialEquiv_symm_apply, cosPartialEquiv_target, cos_arccos, cos_arcsin, cos_arcsin_nonneg, injOn_arcsin, le_arcsin_iff_sin_le, le_arcsin_iff_sin_le', lt_arcsin_iff_sin_lt, lt_arcsin_iff_sin_lt', mapsTo_cos_Ioo, mapsTo_sin_Ioo, monotone_arcsin, neg_pi_div_two_eq_arcsin, neg_pi_div_two_le_arcsin, neg_pi_div_two_lt_arcsin, pi_div_four_le_arcsin, pi_div_two_eq_arcsin, pi_div_two_le_arcsin, range_arcsin, sin_arccos, sin_arcsin, sin_arcsin', strictAntiOn_arccos, strictMonoOn_arcsin, tan_arccos, tan_arcsin, zero_eq_arcsin_iff	105
Total	111

Continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arccos 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arccos	—	comp Real.continuous_arccos
arcsin 📖	mathematical	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arcsin	—	comp Real.continuous_arcsin

ContinuousAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arccos 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arccos	—	Filter.Tendsto.arccos
arcsin 📖	mathematical	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arcsin	—	Filter.Tendsto.arcsin

ContinuousOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arccos 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arccos	—	ContinuousWithinAt.arccos
arcsin 📖	mathematical	ContinuousOn Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arcsin	—	ContinuousWithinAt.arcsin

ContinuousWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arccos 📖	mathematical	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arccos	—	Filter.Tendsto.arccos
arcsin 📖	mathematical	ContinuousWithinAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arcsin	—	Filter.Tendsto.arcsin

Filter.Tendsto

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
arccos 📖	mathematical	Filter.Tendsto Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arccos	—	comp Continuous.tendsto Real.continuous_arccos
arccos_nhdsGE 📖	mathematical	Filter.Tendsto Real nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ici Real.instPreorder	Real.arccos Set.Iic	—	comp inf Continuous.tendsto Real.continuous_arccos Set.MapsTo.tendsto Real.antitone_arccos
arccos_nhdsLE 📖	mathematical	Filter.Tendsto Real nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Iic Real.instPreorder	Real.arccos Set.Ici	—	comp inf Continuous.tendsto Real.continuous_arccos Set.MapsTo.tendsto Real.arccos_le_arccos
arcsin 📖	mathematical	Filter.Tendsto Real nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	Real.arcsin	—	comp Continuous.tendsto Real.continuous_arcsin
arcsin_nhdsGE 📖	mathematical	Filter.Tendsto Real nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Ici Real.instPreorder	Real.arcsin	—	comp inf Continuous.tendsto Real.continuous_arcsin Set.MapsTo.tendsto Real.arcsin_le_arcsin
arcsin_nhdsLE 📖	mathematical	Filter.Tendsto Real nhdsWithin UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Set.Iic Real.instPreorder	Real.arcsin	—	comp inf Continuous.tendsto Real.continuous_arcsin Set.MapsTo.tendsto Real.monotone_arcsin

Real

Definitions

Name	Category	Theorems
arccos 📖	CompOp	72 math math: arctan_eq_arccos, hasDerivAt_arccos, arcsin_eq_pi_div_two_sub_arccos, InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero, ContinuousWithinAt.arccos, Filter.Tendsto.arccos_nhdsGE, strictAntiOn_arccos, deriv_arccos, differentiableWithinAt_arccos_Ici, Filter.Tendsto.arccos, Orientation.oangle_sub_right_eq_arccos_of_oangle_eq_pi_div_two, tan_arccos, arccos_pos, ContinuousAt.arccos, hasStrictDerivAt_arccos, arccos_one, arccos_eq_zero, arccos_eq_pi_div_two_sub_arcsin, Complex.arg_of_im_pos, arccos_image_Icc, Filter.Tendsto.arccos_nhdsLE, hasDerivWithinAt_arccos_Ici, arccos_le_pi, arccos_le_pi_div_two, arccos_inj, arccos_eq_pi_div_two, arccos_neg, arcsin_eq_arccos, arccos_le_pi_div_four, arccos_eq_arcsin, antitone_arccos, Complex.arg_eq_nhds_of_im_neg, Complex.arg_of_im_nonneg_of_ne_zero, Orientation.oangle_sub_left_eq_arccos_of_oangle_eq_pi_div_two, unitary.norm_argSelfAdjoint, arccos_eq_pi, arccos_eq_of_eq_cos, Continuous.arccos, EuclideanGeometry.oangle_left_eq_arccos_of_oangle_eq_pi_div_two, measurable_arccos, arccos_eq_arctan, arccos_lt_pi, EuclideanGeometry.angle_eq_arccos_of_angle_eq_pi_div_two, cos_arccos, differentiableOn_arccos, differentiableWithinAt_arccos_Iic, contDiffOn_arccos, InnerProductGeometry.angle_add_eq_arccos_of_inner_eq_zero, Complex.arg_of_im_neg, differentiableAt_arccos, sin_arccos, arccos_cos, arccos_of_le_neg_one, cosPartialEquiv_symm_apply, ContinuousOn.arccos, arccos_lt_pi_div_two, arccos_neg_one, Complex.arg_eq_nhds_of_im_pos, contDiffAt_arccos, arccos_lt_arccos, EuclideanGeometry.oangle_right_eq_arccos_of_oangle_eq_pi_div_two, Unitary.norm_argSelfAdjoint, arccos_zero, arccos_nonneg, arccos_le_arccos, Orientation.oangle_add_left_eq_arccos_of_oangle_eq_pi_div_two, arccos_of_one_le, continuous_arccos, hasDerivWithinAt_arccos_Iic, contDiffAt_arccos_iff, Orientation.oangle_add_right_eq_arccos_of_oangle_eq_pi_div_two, arccos_injOn
arcsin 📖	CompOp	94 math math: pi_div_four_le_arcsin, differentiableAt_arcsin, arcsin_eq_pi_div_two_sub_arccos, arctan_eq_arcsin, neg_pi_div_two_eq_arcsin, ContinuousWithinAt.arcsin, Complex.arg_of_re_nonneg, continuous_arcsin, differentiableOn_arcsin, Filter.Tendsto.arcsin, arcsin_nonpos, Orientation.oangle_add_right_eq_arcsin_of_oangle_eq_pi_div_two, monotone_arcsin, sin_arcsin, cos_arcsin, EuclideanGeometry.oangle_right_eq_arcsin_of_oangle_eq_pi_div_two, Complex.arg_of_re_neg_of_im_nonneg, arcsin_eq_pi_div_two, arccos_eq_pi_div_two_sub_arcsin, arcsin_le_pi_div_two, pi_div_two_eq_arcsin, sin_arcsin', Filter.Tendsto.arcsin_nhdsGE, le_arcsin_iff_sin_le', zero_eq_arcsin_iff, arcsin_neg_one, arcsin_le_arcsin, arcsin_mem_Icc, hasDerivAt_arcsin, Complex.arg_of_re_neg_of_im_neg, arcsin_eq_arccos, Orientation.oangle_sub_left_eq_arcsin_of_oangle_eq_pi_div_two, arcsin_lt_iff_lt_sin, arccos_eq_arcsin, arcsin_le_iff_le_sin', Orientation.oangle_add_left_eq_arcsin_of_oangle_eq_pi_div_two, contDiffAt_arcsin_iff, arcsin_neg, differentiableWithinAt_arcsin_Ici, hasDerivWithinAt_arcsin_Ici, injOn_arcsin, continuousAt_arcsin, cos_arcsin_nonneg, arcsin_of_le_neg_one, range_arcsin, arcsin_eq_of_sin_eq, arcsin_le_neg_pi_div_two, arcsin_eq_zero_iff, lt_arcsin_iff_sin_lt, Orientation.oangle_sub_right_eq_arcsin_of_oangle_eq_pi_div_two, lt_arcsin_iff_sin_lt', EuclideanGeometry.oangle_left_eq_arcsin_of_oangle_eq_pi_div_two, differentiableWithinAt_arcsin_Iic, deriv_arcsin, ContinuousOn.arcsin, strictMonoOn_arcsin, arcsin_of_one_le, arcsin_lt_zero, measurable_arcsin, neg_pi_div_two_lt_arcsin, arcsin_sin, EuclideanGeometry.angle_eq_arcsin_of_angle_eq_pi_div_two, arcsin_nonneg, arcsin_lt_iff_lt_sin', pi_div_two_le_arcsin, le_arcsin_iff_sin_le, hasStrictDerivAt_arcsin, ContinuousAt.arcsin, InnerProductGeometry.angle_sub_eq_arcsin_of_inner_eq_zero, arcsin_lt_pi_div_two, arcsin_pos, arcsin_sin', arcsin_image_Icc, Complex.arg_eq_nhds_of_re_pos, neg_pi_div_two_le_arcsin, arcsin_eq_iff_eq_sin, arcsin_zero, Complex.arg_eq_nhds_of_re_neg_of_im_pos, arcsin_inj, deriv_arcsin_aux, Complex.arg_eq_nhds_of_re_neg_of_im_neg, arcsin_eq_arctan, arcsin_le_iff_le_sin, tan_arcsin, arcsin_eq_neg_pi_div_two, contDiffAt_arcsin, InnerProductGeometry.angle_add_eq_arcsin_of_inner_eq_zero, Continuous.arcsin, contDiffOn_arcsin, Filter.Tendsto.arcsin_nhdsLE, arcsin_lt_arcsin, arcsin_projIcc, hasDerivWithinAt_arcsin_Iic, arcsin_one
cosPartialEquiv 📖	CompOp	4 math math: cosPartialEquiv_target, cosPartialEquiv_apply, cosPartialEquiv_symm_apply, cosPartialEquiv_source
cosPartialHomeomorph 📖	CompOp	—
sinPartialEquiv 📖	CompOp	—
sinPartialHomeomorph 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone_arccos 📖	mathematical	—	Antitone Real instPreorder arccos	—	arccos_le_arccos
arccos_cos 📖	mathematical	Real instLE instZero pi	arccos cos	—	arccos.eq_1 Nat.instAtLeastTwoHAddOfNat sin_pi_div_two_sub arcsin_sin sub_eq_add_neg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid add_halves CharZero.NeZero.two RCLike.charZero_rclike 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.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_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero 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 IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le neg_add_rev neg_neg add_neg_cancel_comm_assoc
arccos_eq_arcsin 📖	mathematical	Real instLE instZero	arccos arcsin sqrt instSub instOne Monoid.toNatPow instMonoid	—	arcsin_eq_of_sin_eq sin_arccos Nat.instAtLeastTwoHAddOfNat LE.le.trans Left.neg_nonpos_iff IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid div_nonneg PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing LT.lt.le pi_pos instIsOrderedRing arccos_nonneg arccos_le_pi_div_two
arccos_eq_of_eq_cos 📖	mathematical	Real instLE instZero pi cos	arccos	—	arccos_cos
arccos_eq_pi 📖	mathematical	—	arccos pi Real instLE instNeg instOne	—	arccos.eq_1 sub_eq_iff_eq_add sub_eq_iff_eq_add' Nat.instAtLeastTwoHAddOfNat div_two_sub_self instIsStrictOrderedRing neg_pi_div_two_eq_arcsin
arccos_eq_pi_div_two 📖	mathematical	—	arccos Real DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instZero	—	Nat.instAtLeastTwoHAddOfNat
arccos_eq_pi_div_two_sub_arcsin 📖	mathematical	—	arccos Real instSub DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arcsin	—	—
arccos_eq_zero 📖	mathematical	—	arccos Real instZero instLE instOne	—	—
arccos_image_Icc 📖	mathematical	—	Set.image Real arccos Set.Icc instPreorder instNeg instOne instZero pi	—	Set.image_congr PartialEquiv.image_source_eq_target
arccos_inj 📖	mathematical	Real instLE instNeg instOne	arccos	—	Set.InjOn.eq_iff arccos_injOn
arccos_injOn 📖	mathematical	—	Set.InjOn Real arccos Set.Icc instPreorder instNeg instOne	—	StrictAntiOn.injOn strictAntiOn_arccos
arccos_le_arccos 📖	mathematical	Real instLE	arccos	—	sub_le_sub_left IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add arcsin_le_arcsin
arccos_le_pi 📖	mathematical	—	Real instLE arccos pi	—	le_of_not_gt 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.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_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.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.isInt_add Mathlib.Tactic.Ring.neg_congr 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_neg_of_le 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 Mathlib.Tactic.Linarith.mul_neg Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true CancelDenoms.neg_subst Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le neg_pi_div_two_le_arcsin
arccos_le_pi_div_four 📖	mathematical	—	Real instLE arccos DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat sqrt	—	Nat.instAtLeastTwoHAddOfNat arccos.eq_1 pi_div_four_le_arcsin le_of_not_gt 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.mul_one 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 Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_add_gt 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 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 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
arccos_le_pi_div_two 📖	mathematical	—	Real instLE arccos DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instZero	—	Nat.instAtLeastTwoHAddOfNat AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le
arccos_lt_arccos 📖	mathematical	Real instLE instNeg instOne instLT	arccos	—	sub_lt_sub_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add arcsin_lt_arcsin
arccos_lt_pi 📖	mathematical	—	Real instLT arccos pi instNeg instOne	—	—
arccos_lt_pi_div_two 📖	mathematical	—	Real instLT arccos DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instZero	—	Nat.instAtLeastTwoHAddOfNat IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
arccos_neg 📖	mathematical	—	arccos Real instNeg instSub pi	—	Nat.instAtLeastTwoHAddOfNat add_halves CharZero.NeZero.two RCLike.charZero_rclike arccos.eq_1 arcsin_neg add_sub_assoc sub_sub_self sub_neg_eq_add
arccos_neg_one 📖	mathematical	—	arccos Real instNeg instOne pi	—	Nat.instAtLeastTwoHAddOfNat arcsin_neg arcsin_one sub_neg_eq_add add_halves CharZero.NeZero.two RCLike.charZero_rclike
arccos_nonneg 📖	mathematical	—	Real instLE instZero arccos	—	le_of_not_gt 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.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.cast_zero Nat.cast_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le 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 Mathlib.Tactic.Linarith.mul_neg Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le arcsin_le_pi_div_two
arccos_of_le_neg_one 📖	mathematical	Real instLE instNeg instOne	arccos pi	—	arccos.eq_1 Nat.instAtLeastTwoHAddOfNat arcsin_of_le_neg_one sub_neg_eq_add add_halves CharZero.NeZero.two RCLike.charZero_rclike
arccos_of_one_le 📖	mathematical	Real instLE instOne	arccos instZero	—	arccos.eq_1 Nat.instAtLeastTwoHAddOfNat arcsin_of_one_le sub_self
arccos_one 📖	mathematical	—	arccos Real instOne instZero	—	Nat.instAtLeastTwoHAddOfNat arcsin_one sub_self
arccos_pos 📖	mathematical	—	Real instLT instZero arccos instOne	—	IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
arccos_zero 📖	mathematical	—	arccos Real instZero DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat arcsin_zero sub_zero
arcsin_eq_arccos 📖	mathematical	Real instLE instZero	arcsin arccos sqrt instSub instOne Monoid.toNatPow instMonoid	—	cos_arcsin arccos_cos arcsin_nonneg LE.le.trans Nat.instAtLeastTwoHAddOfNat arcsin_le_pi_div_two div_le_self PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono instIsStrictOrderedRing LT.lt.le pi_pos one_le_two instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid
arcsin_eq_iff_eq_sin 📖	mathematical	Real Set Set.instMembership Set.Ioo instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	arcsin sin	—	Nat.instAtLeastTwoHAddOfNat arcsin_le_iff_le_sin' Set.mem_Ico_of_Ioo le_arcsin_iff_sin_le' Set.mem_Ioc_of_Ioo
arcsin_eq_neg_pi_div_two 📖	mathematical	—	arcsin Real instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instLE instOne	—	Nat.instAtLeastTwoHAddOfNat not_lt LT.lt.ne' neg_pi_div_two_lt_arcsin arcsin_of_le_neg_one
arcsin_eq_of_sin_eq 📖	mathematical	sin Real Set Set.instMembership Set.Icc instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	arcsin	—	Nat.instAtLeastTwoHAddOfNat injOn_sin arcsin_mem_Icc sin_arcsin' sin_mem_Icc
arcsin_eq_pi_div_two 📖	mathematical	—	arcsin Real DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instLE instOne	—	Nat.instAtLeastTwoHAddOfNat not_lt LT.lt.ne arcsin_lt_pi_div_two arcsin_of_one_le
arcsin_eq_pi_div_two_sub_arccos 📖	mathematical	—	arcsin Real instSub DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arccos	—	Nat.instAtLeastTwoHAddOfNat sub_sub_cancel
arcsin_eq_zero_iff 📖	mathematical	—	arcsin Real instZero	—	—
arcsin_image_Icc 📖	mathematical	—	Set.image Real arcsin Set.Icc instPreorder instNeg instOne DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Set.image_congr PartialEquiv.image_source_eq_target
arcsin_inj 📖	mathematical	Real instLE instNeg instOne	arcsin	—	Set.InjOn.eq_iff injOn_arcsin
arcsin_le_arcsin 📖	mathematical	Real instLE	arcsin	—	monotone_arcsin
arcsin_le_iff_le_sin 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder instNeg instOne DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instLE arcsin sin	—	Nat.instAtLeastTwoHAddOfNat arcsin_sin' StrictMonoOn.le_iff_le strictMonoOn_arcsin sin_mem_Icc
arcsin_le_iff_le_sin' 📖	mathematical	Real Set Set.instMembership Set.Ico instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instLE arcsin sin	—	Nat.instAtLeastTwoHAddOfNat le_total arcsin_of_le_neg_one LE.le.trans neg_one_le_sin lt_or_ge arcsin_of_one_le LT.lt.le LT.lt.not_ge LE.le.trans_lt sin_le_one arcsin_le_iff_le_sin Set.mem_Icc_of_Ico
arcsin_le_neg_pi_div_two 📖	mathematical	—	Real instLE arcsin instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	—	Nat.instAtLeastTwoHAddOfNat LE.le.ge_iff_eq' neg_pi_div_two_le_arcsin arcsin_eq_neg_pi_div_two
arcsin_le_pi_div_two 📖	mathematical	—	Real instLE arcsin DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat arcsin_mem_Icc
arcsin_lt_arcsin 📖	mathematical	Real instLE instNeg instOne instLT	arcsin	—	strictMonoOn_arcsin LE.le.trans LT.lt.le
arcsin_lt_iff_lt_sin 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder instNeg instOne DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instLT arcsin sin	—	Nat.instAtLeastTwoHAddOfNat not_le le_arcsin_iff_sin_le
arcsin_lt_iff_lt_sin' 📖	mathematical	Real Set Set.instMembership Set.Ioc instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instLT arcsin sin	—	Nat.instAtLeastTwoHAddOfNat not_le le_arcsin_iff_sin_le'
arcsin_lt_pi_div_two 📖	mathematical	—	Real instLT arcsin DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	—	Nat.instAtLeastTwoHAddOfNat arcsin_lt_iff_lt_sin' Set.right_mem_Ioc neg_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid pi_div_two_pos sin_pi_div_two
arcsin_lt_zero 📖	mathematical	—	Real instLT arcsin instZero	—	lt_iff_lt_of_le_iff_le arcsin_nonneg
arcsin_mem_Icc 📖	mathematical	—	Real Set Set.instMembership Set.Icc instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arcsin	—	Subtype.coe_prop Nat.instAtLeastTwoHAddOfNat
arcsin_neg 📖	mathematical	—	arcsin Real instNeg	—	le_total Nat.instAtLeastTwoHAddOfNat arcsin_of_le_neg_one neg_neg arcsin_of_one_le le_neg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add neg_le_neg arcsin_eq_of_sin_eq sin_neg sin_arcsin arcsin_le_pi_div_two neg_le neg_pi_div_two_le_arcsin
arcsin_neg_one 📖	mathematical	—	arcsin Real instNeg instOne DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	arcsin_eq_of_sin_eq Nat.instAtLeastTwoHAddOfNat sin_neg sin_pi_div_two Set.left_mem_Icc neg_le_self IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LT.lt.le pi_div_two_pos
arcsin_nonneg 📖	mathematical	—	Real instLE instZero arcsin	—	le_arcsin_iff_sin_le' Nat.instAtLeastTwoHAddOfNat neg_lt_zero IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid pi_div_two_pos LT.lt.le sin_zero
arcsin_nonpos 📖	mathematical	—	Real instLE arcsin instZero	—	neg_nonneg IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid arcsin_nonneg arcsin_neg
arcsin_of_le_neg_one 📖	mathematical	Real instLE instNeg instOne	arcsin DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat neg_le_self IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid zero_le_one instZeroLEOneClass arcsin_projIcc Set.left_mem_Icc Set.projIcc_of_le_left arcsin_neg_one
arcsin_of_one_le 📖	mathematical	Real instLE instOne	arcsin DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat neg_le_self IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid zero_le_one instZeroLEOneClass arcsin_projIcc Set.right_mem_Icc Set.projIcc_of_right_le arcsin_one
arcsin_one 📖	mathematical	—	arcsin Real instOne DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	arcsin_eq_of_sin_eq Nat.instAtLeastTwoHAddOfNat sin_pi_div_two Set.right_mem_Icc neg_le_self IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LT.lt.le pi_div_two_pos
arcsin_pos 📖	mathematical	—	Real instLT instZero arcsin	—	lt_iff_lt_of_le_iff_le arcsin_nonpos
arcsin_projIcc 📖	mathematical	—	arcsin Real Set Set.instMembership Set.Icc PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder linearOrder NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid instAddGroup instOne Set.projIcc neg_le_self IsOrderedAddMonoid.toAddLeftMono instAddCommMonoid partialOrder instIsOrderedAddMonoid zero_le_one NegZeroClass.toZero Preorder.toLE instZeroLEOneClass	—	neg_le_self IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid zero_le_one instZeroLEOneClass arcsin.eq_1 Set.IccExtend_val Set.IccExtend.eq_1
arcsin_sin 📖	mathematical	Real instLE instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	arcsin sin	—	Nat.instAtLeastTwoHAddOfNat arcsin_sin'
arcsin_sin' 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	arcsin sin	—	Nat.instAtLeastTwoHAddOfNat injOn_sin arcsin_mem_Icc sin_arcsin neg_one_le_sin sin_le_one
arcsin_zero 📖	mathematical	—	arcsin Real instZero	—	arcsin_eq_of_sin_eq sin_zero Nat.instAtLeastTwoHAddOfNat neg_nonpos IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid LT.lt.le pi_div_two_pos
continuousAt_arcsin 📖	mathematical	—	ContinuousAt Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arcsin	—	Continuous.continuousAt continuous_arcsin
continuous_arccos 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arccos	—	Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal continuous_const continuous_arcsin
continuous_arcsin 📖	mathematical	—	Continuous Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace pseudoMetricSpace arcsin	—	Continuous.comp continuous_subtype_val Continuous.Icc_extend' Nat.instAtLeastTwoHAddOfNat instOrderTopologyReal OrderIso.continuous orderTopology_of_ordConnected Set.ordConnected_Icc
cosPartialEquiv_apply 📖	mathematical	—	PartialEquiv.toFun Real cosPartialEquiv cos	—	—
cosPartialEquiv_source 📖	mathematical	—	PartialEquiv.source Real cosPartialEquiv Set.Icc instPreorder instZero pi	—	—
cosPartialEquiv_symm_apply 📖	mathematical	—	PartialEquiv.toFun Real PartialEquiv.symm cosPartialEquiv arccos	—	—
cosPartialEquiv_target 📖	mathematical	—	PartialEquiv.target Real cosPartialEquiv Set.Icc instPreorder instNeg instOne	—	—
cos_arccos 📖	mathematical	Real instLE instNeg instOne	cos arccos	—	arccos.eq_1 Nat.instAtLeastTwoHAddOfNat cos_pi_div_two_sub sin_arcsin
cos_arcsin 📖	mathematical	—	cos arcsin sqrt Real instSub instOne Monoid.toNatPow instMonoid	—	sin_sq_add_cos_sq sqrt_mul_self cos_arcsin_nonneg sq sq_nonneg AddGroup.existsAddOfLE IsOrderedRing.toPosMulMono instIsOrderedRing IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid sub_nonneg covariant_swap_add_of_covariant_add sin_sq_le_one eq_sub_iff_add_eq' sin_arcsin Nat.instAtLeastTwoHAddOfNat arcsin_of_one_le LT.lt.le not_le cos_pi_div_two sqrt_eq_zero_of_nonpos 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_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.cast_pos Nat.cast_one 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right 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_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_nonneg_of_nonpos_of_nonpos IsOrderedRing.toMulPosMono IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le le_of_lt arcsin_of_le_neg_one cos_neg Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike mul_pos_of_neg_of_neg IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono
cos_arcsin_nonneg 📖	mathematical	—	Real instLE instZero cos arcsin	—	cos_nonneg_of_mem_Icc Nat.instAtLeastTwoHAddOfNat neg_pi_div_two_le_arcsin arcsin_le_pi_div_two
injOn_arcsin 📖	mathematical	—	Set.InjOn Real arcsin Set.Icc instPreorder instNeg instOne	—	StrictMonoOn.injOn strictMonoOn_arcsin
le_arcsin_iff_sin_le 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	instLE arcsin sin	—	Nat.instAtLeastTwoHAddOfNat neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add arcsin_neg arcsin_le_iff_le_sin neg_le_neg neg_le sin_neg
le_arcsin_iff_sin_le' 📖	mathematical	Real Set Set.instMembership Set.Ioc instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instLE arcsin sin	—	Nat.instAtLeastTwoHAddOfNat neg_le_neg_iff IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid covariant_swap_add_of_covariant_add arcsin_neg arcsin_le_iff_le_sin' neg_le_neg neg_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd sin_neg
lt_arcsin_iff_sin_lt 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	instLT arcsin sin	—	Nat.instAtLeastTwoHAddOfNat not_le arcsin_le_iff_le_sin
lt_arcsin_iff_sin_lt' 📖	mathematical	Real Set Set.instMembership Set.Ico instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	instLT arcsin sin	—	Nat.instAtLeastTwoHAddOfNat not_le arcsin_le_iff_le_sin'
mapsTo_cos_Ioo 📖	mathematical	—	Set.MapsTo Real cos Set.Ioo instPreorder instZero pi instNeg instOne	—	PartialEquiv.map_source'
mapsTo_sin_Ioo 📖	mathematical	—	Set.MapsTo Real sin Set.Ioo instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat instOne	—	PartialEquiv.map_source'
monotone_arcsin 📖	mathematical	—	Monotone Real instPreorder arcsin	—	Monotone.comp Subtype.mono_coe Monotone.IccExtend Nat.instAtLeastTwoHAddOfNat OrderIso.monotone
neg_pi_div_two_eq_arcsin 📖	mathematical	—	Real instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arcsin instLE instOne	—	Nat.instAtLeastTwoHAddOfNat arcsin_eq_neg_pi_div_two
neg_pi_div_two_le_arcsin 📖	mathematical	—	Real instLE instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arcsin	—	Nat.instAtLeastTwoHAddOfNat arcsin_mem_Icc
neg_pi_div_two_lt_arcsin 📖	mathematical	—	Real instLT instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arcsin instOne	—	Nat.instAtLeastTwoHAddOfNat lt_arcsin_iff_sin_lt' Set.left_mem_Ico neg_lt_self IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid pi_div_two_pos sin_neg sin_pi_div_two
pi_div_four_le_arcsin 📖	mathematical	—	Real instLE DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arcsin sqrt	—	Nat.instAtLeastTwoHAddOfNat sin_pi_div_four le_arcsin_iff_sin_le' pi_pos 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.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Nat.cast_zero 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_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Nat.cast_one Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one 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_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike 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 Mathlib.Meta.NormNum.isNat_mul CancelDenoms.neg_subst Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le le_of_not_gt Mathlib.Tactic.Linarith.add_neg
pi_div_two_eq_arcsin 📖	mathematical	—	Real DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arcsin instLE instOne	—	Nat.instAtLeastTwoHAddOfNat arcsin_eq_pi_div_two
pi_div_two_le_arcsin 📖	mathematical	—	Real instLE DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat arcsin instOne	—	Nat.instAtLeastTwoHAddOfNat LE.le.ge_iff_eq' arcsin_le_pi_div_two pi_div_two_eq_arcsin
range_arcsin 📖	mathematical	—	Set.range Real arcsin Set.Icc instPreorder instNeg DivInvMonoid.toDiv instDivInvMonoid pi instOfNatAtLeastTwo instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat arcsin.eq_1 Set.range_comp Set.image_congr Set.IccExtend_range EquivLike.range_eq_univ Set.image_univ Subtype.range_coe_subtype
sin_arccos 📖	mathematical	—	sin arccos sqrt Real instSub instOne Monoid.toNatPow instMonoid	—	Nat.instAtLeastTwoHAddOfNat arccos_eq_pi_div_two_sub_arcsin sin_pi_div_two_sub cos_arcsin arccos_of_one_le LT.lt.le not_le sin_zero sqrt_eq_zero_of_nonpos 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_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.cast_pos Nat.cast_one 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right 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_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono 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 le_of_lt arccos_of_le_neg_one sin_pi Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike mul_pos_of_neg_of_neg IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono
sin_arcsin 📖	mathematical	Real instLE instNeg instOne	sin arcsin	—	sin_arcsin'
sin_arcsin' 📖	mathematical	Real Set Set.instMembership Set.Icc instPreorder instNeg instOne	sin arcsin	—	Set.IccExtend_of_mem Nat.instAtLeastTwoHAddOfNat OrderIso.apply_symm_apply
strictAntiOn_arccos 📖	mathematical	—	StrictAntiOn Real instPreorder arccos Set.Icc instNeg instOne	—	sub_lt_sub_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add strictMonoOn_arcsin
strictMonoOn_arcsin 📖	mathematical	—	StrictMonoOn Real instPreorder arcsin Set.Icc instNeg instOne	—	StrictMono.comp_strictMonoOn Subtype.strictMono_coe StrictMono.strictMonoOn_IccExtend Nat.instAtLeastTwoHAddOfNat OrderIso.strictMono
tan_arccos 📖	mathematical	—	tan arccos Real DivInvMonoid.toDiv instDivInvMonoid sqrt instSub instOne Monoid.toNatPow instMonoid	—	arccos.eq_1 Nat.instAtLeastTwoHAddOfNat tan_pi_div_two_sub tan_arcsin inv_div
tan_arcsin 📖	mathematical	—	tan arcsin Real DivInvMonoid.toDiv instDivInvMonoid sqrt instSub instOne Monoid.toNatPow instMonoid	—	tan_eq_sin_div_cos cos_arcsin sin_arcsin sqrt_eq_zero_of_nonpos 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_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.cast_pos Nat.cast_one 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.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right 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_lt_of_neg_of_le instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt instIsOrderedRing Mathlib.Tactic.Linarith.sub_nonpos_of_le mul_nonneg_of_nonpos_of_nonpos AddGroup.existsAddOfLE IsOrderedRing.toMulPosMono 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 le_of_lt lt_of_not_ge div_zero Nat.instAtLeastTwoHAddOfNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Linarith.add_neg Mathlib.Tactic.Linarith.mul_neg Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike mul_pos_of_neg_of_neg IsStrictOrderedRing.toMulPosStrictMono IsRightCancelAdd.addRightStrictMono_of_addRightMono
zero_eq_arcsin_iff 📖	mathematical	—	Real instZero arcsin	—	arcsin_eq_zero_iff

---

← Back to Index