The arctan function.

Inequalities, derivatives, and Real.tan as a LocalHomeomorph between (-(π / 2), π / 2) and the whole line.

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) : Real.tan (x + y) = (Real.tan x + Real.tan y) / (1 - Real.tan x * Real.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) : Real.tan (x + y) = (Real.tan x + Real.tan y) / (1 - Real.tan x * Real.tan y)

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

theorem Real.tan_ne_zero_iff {θ : ℝ} : Real.tan θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * Real.pi / 2

theorem Real.tan_eq_zero_iff {θ : ℝ} : Real.tan θ = 0 ↔ ∃ k, θ = ↑k * Real.pi / 2

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

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

theorem Real.continuous_tan : Continuous fun x => Real.tan ↑x

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

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

theorem Real.tan_surjective : Function.Surjective Real.tan

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

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 : ℝ) : Real.tan (Real.arctan x) = x

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Real.arctan_zero : Real.arctan 0 = 0

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

@[simp]

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

@[simp]

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

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

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

theorem Real.continuous_arctan : Continuous Real.arctan

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

def Real.tanLocalHomeomorph : LocalHomeomorph ℝ ℝ

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

@[simp]

theorem Real.coe_tanLocalHomeomorph : ↑Real.tanLocalHomeomorph = Real.tan

@[simp]

theorem Real.coe_tanLocalHomeomorph_symm : ↑(LocalHomeomorph.symm Real.tanLocalHomeomorph) = Real.arctan