The arctan function.

Inequalities, identities and Real.tan as an OpenPartialHomeomorph between (-(π / 2), π / 2) and the whole line.

The result of arctan x + arctan y is given by arctan_add, arctan_add_eq_add_pi or arctan_add_eq_sub_pi depending on whether x * y < 1 and 0 < x. As an application of arctan_add we give four Machin-like formulas (linear combinations of arctangents equal to π / 4 = arctan 1), including John Machin's original one at four_mul_arctan_inv_5_sub_arctan_inv_239.

theorem Real.tan_add {x y : ℝ} (h : ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) ∨ (∃ (k : ℤ), x = (2 * ↑k + 1) * Real.pi / 2) ∧ ∃ (l : ℤ), y = (2 * ↑l + 1) * Real.pi / 2) : tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

theorem Real.tan_add' {x y : ℝ} (h : (∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) : tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)

theorem Real.tan_sub {x y : ℝ} (h : ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) ∨ (∃ (k : ℤ), x = (2 * ↑k + 1) * Real.pi / 2) ∧ ∃ (l : ℤ), y = (2 * ↑l + 1) * Real.pi / 2) : tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

theorem Real.tan_sub' {x y : ℝ} (h : (∀ (k : ℤ), x ≠ (2 * ↑k + 1) * Real.pi / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * Real.pi / 2) : tan (x - y) = (tan x - tan y) / (1 + tan x * tan y)

theorem Real.tan_two_mul {x : ℝ} : tan (2 * x) = 2 * tan x / (1 - tan x ^ 2)

theorem Real.tan_int_mul_pi_div_two (n : ℤ) : tan (↑n * Real.pi / 2) = 0

theorem Real.continuousOn_tan : ContinuousOn tan {x : ℝ | cos x ≠ 0}

theorem Real.continuous_tan : Continuous fun (x : ↑{x : ℝ | cos x ≠ 0}) => tan ↑x

theorem Real.continuousOn_tan_Ioo : ContinuousOn tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2))

theorem Real.surjOn_tan : Set.SurjOn tan (Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) Set.univ

theorem Real.tan_surjective : Function.Surjective tan

theorem Real.image_tan_Ioo : tan '' Set.Ioo (-(Real.pi / 2)) (Real.pi / 2) = Set.univ

noncomputable def Real.tanOrderIso : ↑(Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) ≃o ℝ

Real.tan as an OrderIso between (-(π / 2), π / 2) and ℝ.

noncomputable def Real.arctan (x : ℝ) : ℝ

Inverse of the tan function, returns values in the range -π / 2 < arctan x and arctan x < π / 2

@[simp]

theorem Real.tan_arctan (x : ℝ) : tan (arctan x) = x

theorem Real.arctan_mem_Ioo (x : ℝ) : arctan x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)

@[simp]

theorem Real.range_arctan : Set.range arctan = Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)

theorem Real.arctan_tan {x : ℝ} (hx₁ : -(Real.pi / 2) < x) (hx₂ : x < Real.pi / 2) : arctan (tan x) = x

theorem Real.cos_arctan_pos (x : ℝ) : 0 < cos (arctan x)

theorem Real.sin_sq_arctan (x : ℝ) : sin (arctan x) ^ 2 = x ^ 2 / (1 + x ^ 2)

theorem Real.cos_sq_arctan (x : ℝ) : cos (arctan x) ^ 2 = 1 / (1 + x ^ 2)

theorem Real.sin_arctan (x : ℝ) : sin (arctan x) = x / √(1 + x ^ 2)

theorem Real.cos_arctan (x : ℝ) : cos (arctan x) = 1 / √(1 + x ^ 2)

theorem Real.arctan_lt_pi_div_two (x : ℝ) : arctan x < Real.pi / 2

theorem Real.neg_pi_div_two_lt_arctan (x : ℝ) : -(Real.pi / 2) < arctan x

theorem Real.arctan_eq_arcsin (x : ℝ) : arctan x = arcsin (x / √(1 + x ^ 2))

theorem Real.arcsin_eq_arctan {x : ℝ} (h : x ∈ Set.Ioo (-1) 1) : arcsin x = arctan (x / √(1 - x ^ 2))

@[simp]

theorem Real.arctan_zero : arctan 0 = 0

theorem Real.arctan_strictMono : StrictMono arctan

theorem Real.arctan_mono : Monotone arctan

@[deprecated Real.arctan_strictMono (since := "2025-10-20")]

theorem Real.arctan_lt_arctan {x y : ℝ} (hxy : x < y) : arctan x < arctan y

@[simp]

theorem Real.arctan_lt_arctan_iff {x y : ℝ} : arctan x < arctan y ↔ x < y

@[deprecated Real.arctan_mono (since := "2025-10-20")]

theorem Real.arctan_le_arctan {x y : ℝ} (hxy : x ≤ y) : arctan x ≤ arctan y

@[simp]

theorem Real.arctan_le_arctan_iff {x y : ℝ} : arctan x ≤ arctan y ↔ x ≤ y

theorem Real.arctan_injective : Function.Injective arctan

@[simp]

theorem Real.arctan_inj {x y : ℝ} : arctan x = arctan y ↔ x = y

@[simp]

theorem Real.arctan_eq_zero_iff {x : ℝ} : arctan x = 0 ↔ x = 0

theorem Real.tendsto_arctan_atTop : Filter.Tendsto arctan Filter.atTop (nhdsWithin (Real.pi / 2) (Set.Iio (Real.pi / 2)))

theorem Real.tendsto_arctan_atBot : Filter.Tendsto arctan Filter.atBot (nhdsWithin (-(Real.pi / 2)) (Set.Ioi (-(Real.pi / 2))))

theorem Real.arctan_eq_of_tan_eq {x y : ℝ} (h : tan x = y) (hx : x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)) : arctan y = x

@[simp]

theorem Real.arctan_one : arctan 1 = Real.pi / 4

@[simp]

theorem Real.arctan_sqrt_three : arctan √3 = Real.pi / 3

@[simp]

theorem Real.arctan_inv_sqrt_three : arctan (√3)⁻¹ = Real.pi / 6

@[simp]

theorem Real.arctan_eq_pi_div_four {x : ℝ} : arctan x = Real.pi / 4 ↔ x = 1

@[simp]

theorem Real.arctan_neg (x : ℝ) : arctan (-x) = -arctan x

@[simp]

theorem Real.arctan_eq_neg_pi_div_four {x : ℝ} : arctan x = -(Real.pi / 4) ↔ x = -1

@[simp]

theorem Real.arctan_pos {x : ℝ} : 0 < arctan x ↔ 0 < x

@[simp]

theorem Real.arctan_lt_zero {x : ℝ} : arctan x < 0 ↔ x < 0

@[simp]

theorem Real.arctan_nonneg {x : ℝ} : 0 ≤ arctan x ↔ 0 ≤ x

@[simp]

theorem Real.arctan_le_zero {x : ℝ} : arctan x ≤ 0 ↔ x ≤ 0

theorem Real.arctan_eq_arccos {x : ℝ} (h : 0 ≤ x) : arctan x = arccos (√(1 + x ^ 2))⁻¹

theorem Real.arccos_eq_arctan {x : ℝ} (h : 0 < x) : arccos x = arctan (√(1 - x ^ 2) / x)

theorem Real.arctan_inv_of_pos {x : ℝ} (h : 0 < x) : arctan x⁻¹ = Real.pi / 2 - arctan x

theorem Real.arctan_inv_of_neg {x : ℝ} (h : x < 0) : arctan x⁻¹ = -(Real.pi / 2) - arctan x

theorem Real.arctan_ne_mul_pi_div_two {x : ℝ} (k : ℤ) : arctan x ≠ (2 * ↑k + 1) * Real.pi / 2

theorem Real.arctan_add_arctan_lt_pi_div_two {x y : ℝ} (h : x * y < 1) : arctan x + arctan y < Real.pi / 2

theorem Real.arctan_add {x y : ℝ} (h : x * y < 1) : arctan x + arctan y = arctan ((x + y) / (1 - x * y))

theorem Real.arctan_add_eq_add_pi {x y : ℝ} (h : 1 < x * y) (hx : 0 < x) : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) + Real.pi

theorem Real.arctan_add_eq_sub_pi {x y : ℝ} (h : 1 < x * y) (hx : x < 0) : arctan x + arctan y = arctan ((x + y) / (1 - x * y)) - Real.pi

theorem Real.two_mul_arctan {x : ℝ} (h₁ : -1 < x) (h₂ : x < 1) : 2 * arctan x = arctan (2 * x / (1 - x ^ 2))

theorem Real.two_mul_arctan_add_pi {x : ℝ} (h : 1 < x) : 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) + Real.pi

theorem Real.two_mul_arctan_sub_pi {x : ℝ} (h : x < -1) : 2 * arctan x = arctan (2 * x / (1 - x ^ 2)) - Real.pi

theorem Real.arctan_inv_2_add_arctan_inv_3 : arctan 2⁻¹ + arctan 3⁻¹ = Real.pi / 4

theorem Real.two_mul_arctan_inv_2_sub_arctan_inv_7 : 2 * arctan 2⁻¹ - arctan 7⁻¹ = Real.pi / 4

theorem Real.two_mul_arctan_inv_3_add_arctan_inv_7 : 2 * arctan 3⁻¹ + arctan 7⁻¹ = Real.pi / 4

theorem Real.four_mul_arctan_inv_5_sub_arctan_inv_239 : 4 * arctan 5⁻¹ - arctan 239⁻¹ = Real.pi / 4

John Machin's 1706 formula, which he used to compute π to 100 decimal places.

theorem Real.sin_arctan_strictMono : StrictMono fun (x : ℝ) => sin (arctan x)

@[simp]

theorem Real.sin_arctan_pos {x : ℝ} : 0 < sin (arctan x) ↔ 0 < x

@[simp]

theorem Real.sin_arctan_lt_zero {x : ℝ} : sin (arctan x) < 0 ↔ x < 0

@[simp]

theorem Real.sin_arctan_eq_zero {x : ℝ} : sin (arctan x) = 0 ↔ x = 0

@[simp]

theorem Real.sin_arctan_nonneg {x : ℝ} : 0 ≤ sin (arctan x) ↔ 0 ≤ x

@[simp]

theorem Real.sin_arctan_le_zero {x : ℝ} : sin (arctan x) ≤ 0 ↔ x ≤ 0

theorem Real.continuous_arctan : Continuous arctan

theorem Real.continuousAt_arctan {x : ℝ} : ContinuousAt arctan x

noncomputable def Real.tanPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ

Real.tan as an OpenPartialHomeomorph between (-(π / 2), π / 2) and the whole line.

@[simp]

theorem Real.coe_tanPartialHomeomorph : ↑tanPartialHomeomorph = tan

@[simp]

theorem Real.coe_tanPartialHomeomorph_symm : ↑tanPartialHomeomorph.symm = arctan

def Mathlib.Meta.Positivity.evalRealArctan : PositivityExt

Extension for Real.arctan.

def Mathlib.Meta.Positivity.evalRealCosArctan : PositivityExt

Extension for Real.cos (Real.arctan _).

def Mathlib.Meta.Positivity.evalRealSinArctan : PositivityExt

Extension for Real.sin (Real.arctan _).