[GOAL]
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ tan (x + y) = (tan x + tan y) / (1 - tan x * tan y)
[PROOFSTEP]
simpa only [← Complex.ofReal_inj, Complex.ofReal_sub, Complex.ofReal_add, Complex.ofReal_div, Complex.ofReal_mul,
  Complex.ofReal_tan] using @Complex.tan_add (x : ℂ) (y : ℂ) (by convert h <;> norm_cast)
[GOAL]
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
⊢ ((∀ (k : ℤ), ↑x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), ↑y ≠ (2 * ↑l + 1) * ↑π / 2) ∨
    (∃ k, ↑x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ l, ↑y = (2 * ↑l + 1) * ↑π / 2
[PROOFSTEP]
convert h
[GOAL]
case h.e'_1.h.e'_1.h.h.a
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
a✝ : ℤ
⊢ ↑x = (2 * ↑a✝ + 1) * ↑π / 2 ↔ x = (2 * ↑a✝ + 1) * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_1.h.e'_2.h.h.a
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
a✝ : ℤ
⊢ ↑y = (2 * ↑a✝ + 1) * ↑π / 2 ↔ y = (2 * ↑a✝ + 1) * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_2.h.e'_1.h.e'_2.h.a
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
x✝ : ℤ
⊢ ↑x = (2 * ↑x✝ + 1) * ↑π / 2 ↔ x = (2 * ↑x✝ + 1) * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
case h.e'_2.h.e'_2.h.e'_2.h.a
x y : ℝ
h :
  ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * π / 2) ∧ ∀ (l : ℤ), y ≠ (2 * ↑l + 1) * π / 2) ∨
    (∃ k, x = (2 * ↑k + 1) * π / 2) ∧ ∃ l, y = (2 * ↑l + 1) * π / 2
x✝ : ℤ
⊢ ↑y = (2 * ↑x✝ + 1) * ↑π / 2 ↔ y = (2 * ↑x✝ + 1) * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
x : ℝ
⊢ tan (2 * x) = ↑2 * tan x / (↑1 - tan x ^ 2)
[PROOFSTEP]
have := @Complex.tan_two_mul x
[GOAL]
x : ℝ
this : Complex.tan (2 * ↑x) = 2 * Complex.tan ↑x / (1 - Complex.tan ↑x ^ 2)
⊢ tan (2 * x) = ↑2 * tan x / (↑1 - tan x ^ 2)
[PROOFSTEP]
norm_cast at *
[GOAL]
θ : ℝ
⊢ tan θ ≠ 0 ↔ ∀ (k : ℤ), θ ≠ ↑k * π / 2
[PROOFSTEP]
rw [← Complex.ofReal_ne_zero, Complex.ofReal_tan, Complex.tan_ne_zero_iff]
[GOAL]
θ : ℝ
⊢ (∀ (k : ℤ), ↑θ ≠ ↑k * ↑π / 2) ↔ ∀ (k : ℤ), θ ≠ ↑k * π / 2
[PROOFSTEP]
norm_cast
[GOAL]
θ : ℝ
⊢ tan θ = 0 ↔ ∃ k, θ = ↑k * π / 2
[PROOFSTEP]
rw [← not_iff_not, not_exists, ← Ne, tan_ne_zero_iff]
[GOAL]
n : ℤ
⊢ ∃ k, ↑n * π / 2 = ↑k * π / 2
[PROOFSTEP]
use n
[GOAL]
⊢ ContinuousOn tan {x | cos x ≠ 0}
[PROOFSTEP]
suffices ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
  by
  have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
  rwa [h_eq] at this 
[GOAL]
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ ContinuousOn tan {x | cos x ≠ 0}
[PROOFSTEP]
have h_eq : (fun x => sin x / cos x) = tan := by ext1 x; rw [tan_eq_sin_div_cos]
[GOAL]
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
⊢ (fun x => sin x / cos x) = tan
[PROOFSTEP]
ext1 x
[GOAL]
case h
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
x : ℝ
⊢ sin x / cos x = tan x
[PROOFSTEP]
rw [tan_eq_sin_div_cos]
[GOAL]
this : ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
h_eq : (fun x => sin x / cos x) = tan
⊢ ContinuousOn tan {x | cos x ≠ 0}
[PROOFSTEP]
rwa [h_eq] at this 
[GOAL]
⊢ ContinuousOn (fun x => sin x / cos x) {x | cos x ≠ 0}
[PROOFSTEP]
exact continuousOn_sin.div continuousOn_cos fun x => id
[GOAL]
⊢ ContinuousOn tan (Ioo (-(π / 2)) (π / 2))
[PROOFSTEP]
refine' ContinuousOn.mono continuousOn_tan fun x => _
[GOAL]
x : ℝ
⊢ x ∈ Ioo (-(π / 2)) (π / 2) → x ∈ {x | cos x ≠ 0}
[PROOFSTEP]
simp only [and_imp, mem_Ioo, mem_setOf_eq, Ne.def]
[GOAL]
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬cos x = 0
[PROOFSTEP]
rw [cos_eq_zero_iff]
[GOAL]
x : ℝ
⊢ -(π / 2) < x → x < π / 2 → ¬∃ k, x = (2 * ↑k + 1) * π / 2
[PROOFSTEP]
rintro hx_gt hx_lt ⟨r, hxr_eq⟩
[GOAL]
case intro
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
⊢ False
[PROOFSTEP]
cases' le_or_lt 0 r with h h
[GOAL]
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False
[PROOFSTEP]
rw [lt_iff_not_ge] at hx_lt 
[GOAL]
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ False
[PROOFSTEP]
refine' hx_lt _
[GOAL]
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ x ≥ π / 2
[PROOFSTEP]
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, ge_iff_le, mul_le_mul_right (half_pos pi_pos)]
[GOAL]
case intro.inl
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : ¬x ≥ π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : 0 ≤ r
⊢ 1 ≤ 2 * ↑r + 1
[PROOFSTEP]
simp [h]
[GOAL]
case intro.inr
x : ℝ
hx_gt : -(π / 2) < x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False
[PROOFSTEP]
rw [lt_iff_not_ge] at hx_gt 
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ False
[PROOFSTEP]
refine' hx_gt _
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ -(π / 2) ≥ x
[PROOFSTEP]
rw [hxr_eq, ← one_mul (π / 2), mul_div_assoc, ge_iff_le, neg_mul_eq_neg_mul, mul_le_mul_right (half_pos pi_pos)]
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ 2 * ↑r + 1 ≤ -1
[PROOFSTEP]
have hr_le : r ≤ -1 := by rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h 
[GOAL]
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
⊢ r ≤ -1
[PROOFSTEP]
rwa [Int.lt_iff_add_one_le, ← le_neg_iff_add_nonpos_right] at h 
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 2 * ↑r + 1 ≤ -1
[PROOFSTEP]
rw [← le_sub_iff_add_le, mul_comm, ← le_div_iff]
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ (-1 - 1) / 2
[PROOFSTEP]
norm_num
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ -1
[PROOFSTEP]
rw [← Int.cast_one, ← Int.cast_neg]
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ ↑r ≤ ↑(-1)
[PROOFSTEP]
norm_cast
[GOAL]
case intro.inr
x : ℝ
hx_gt : ¬-(π / 2) ≥ x
hx_lt : x < π / 2
r : ℤ
hxr_eq : x = (2 * ↑r + 1) * π / 2
h : r < 0
hr_le : r ≤ -1
⊢ 0 < 2
[PROOFSTEP]
exact zero_lt_two
[GOAL]
this : -(π / 2) < π / 2
⊢ Tendsto (fun x => tan ↑x) atBot atBot
[PROOFSTEP]
rw [tendsto_comp_coe_Ioo_atBot this]
[GOAL]
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[Ioi (-(π / 2))] (-(π / 2))) atBot
[PROOFSTEP]
exact tendsto_tan_neg_pi_div_two
[GOAL]
this : -(π / 2) < π / 2
⊢ Tendsto (fun x => tan ↑x) atTop atTop
[PROOFSTEP]
rw [tendsto_comp_coe_Ioo_atTop this]
[GOAL]
this : -(π / 2) < π / 2
⊢ Tendsto tan (𝓝[Iio (π / 2)] (π / 2)) atTop
[PROOFSTEP]
exact tendsto_tan_pi_div_two
[GOAL]
x : ℝ
⊢ cos (arctan x) ^ 2 = ↑1 / (↑1 + x ^ 2)
[PROOFSTEP]
rw_mod_cast [one_div, ← inv_one_add_tan_sq (cos_arctan_pos x).ne', tan_arctan]
[GOAL]
x : ℝ
⊢ sin (arctan x) = x / sqrt (↑1 + x ^ 2)
[PROOFSTEP]
rw_mod_cast [← tan_div_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
[GOAL]
x : ℝ
⊢ cos (arctan x) = ↑1 / sqrt (↑1 + x ^ 2)
[PROOFSTEP]
rw_mod_cast [one_div, ← inv_sqrt_one_add_tan_sq (cos_arctan_pos x), tan_arctan]
[GOAL]
x : ℝ
h : x ∈ Ioo (-1) 1
⊢ arcsin x = arctan (x / sqrt (↑1 - x ^ 2))
[PROOFSTEP]
rw_mod_cast [arctan_eq_arcsin, div_pow, sq_sqrt, one_add_div, div_div, ← sqrt_mul, mul_div_cancel', sub_add_cancel,
  sqrt_one, div_one]
[GOAL]
case hb
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0
[PROOFSTEP]
simp at h 
[GOAL]
case hx
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
[PROOFSTEP]
simp at h 
[GOAL]
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 1 - x ^ 2 ≠ 0
[PROOFSTEP]
simp at h 
[GOAL]
x : ℝ
h : x ∈ Ioo (↑(Int.negSucc 0)) 1
⊢ 0 ≤ 1 - x ^ 2
[PROOFSTEP]
simp at h 
[GOAL]
case hb
x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0
[PROOFSTEP]
nlinarith [h.1, h.2]
[GOAL]
case hx
x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2
[PROOFSTEP]
nlinarith [h.1, h.2]
[GOAL]
x : ℝ
h : -1 < x ∧ x < 1
⊢ 1 - x ^ 2 ≠ 0
[PROOFSTEP]
nlinarith [h.1, h.2]
[GOAL]
x : ℝ
h : -1 < x ∧ x < 1
⊢ 0 ≤ 1 - x ^ 2
[PROOFSTEP]
nlinarith [h.1, h.2]
[GOAL]
⊢ arctan 0 = 0
[PROOFSTEP]
simp [arctan_eq_arcsin]
[GOAL]
x y : ℝ
h : tan x = y
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ tan (arctan y) = tan x
[PROOFSTEP]
rw [tan_arctan, h]
[GOAL]
⊢ π / 4 ∈ Ioo (-(π / 2)) (π / 2)
[PROOFSTEP]
constructor
[GOAL]
case left
⊢ -(π / 2) < π / 4
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
case right
⊢ π / 4 < π / 2
[PROOFSTEP]
linarith [pi_pos]
[GOAL]
x : ℝ
⊢ arctan (-x) = -arctan x
[PROOFSTEP]
simp [arctan_eq_arcsin, neg_div]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arctan x = arccos (sqrt (↑1 + x ^ 2))⁻¹
[PROOFSTEP]
rw [arctan_eq_arcsin, arccos_eq_arcsin]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / sqrt (↑1 + x ^ 2)) = arcsin (sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2))
x : ℝ h : 0 ≤ x ⊢ 0 ≤ (sqrt (↑1 + x ^ 2))⁻¹
[PROOFSTEP]
swap
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (sqrt (↑1 + x ^ 2))⁻¹
[PROOFSTEP]
exact inv_nonneg.2 (sqrt_nonneg _)
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arcsin (x / sqrt (↑1 + x ^ 2)) = arcsin (sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2))
[PROOFSTEP]
congr 1
[GOAL]
case e_a
x : ℝ
h : 0 ≤ x
⊢ x / sqrt (↑1 + x ^ 2) = sqrt (1 - (sqrt (↑1 + x ^ 2))⁻¹ ^ 2)
[PROOFSTEP]
rw_mod_cast [← sqrt_inv, sq_sqrt, ← one_div, one_sub_div, add_sub_cancel', sqrt_div, sqrt_sq h]
[GOAL]
case e_a.hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2
case e_a
x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0
case e_a x : ℝ h : 0 ≤ x ⊢ 0 ≤ (1 + x ^ 2)⁻¹
[PROOFSTEP]
all_goals positivity
[GOAL]
case e_a.hx
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ x ^ 2
[PROOFSTEP]
positivity
[GOAL]
case e_a
x : ℝ
h : 0 ≤ x
⊢ 1 + x ^ 2 ≠ 0
[PROOFSTEP]
positivity
[GOAL]
case e_a
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ (1 + x ^ 2)⁻¹
[PROOFSTEP]
positivity
[GOAL]
x : ℝ
h : 0 < x
⊢ arccos x = arctan (sqrt (↑1 - x ^ 2) / x)
[PROOFSTEP]
rw [arccos, eq_comm]
[GOAL]
x : ℝ
h : 0 < x
⊢ arctan (sqrt (↑1 - x ^ 2) / x) = π / 2 - arcsin x
[PROOFSTEP]
refine' arctan_eq_of_tan_eq _ ⟨_, _⟩
[GOAL]
case refine'_1
x : ℝ
h : 0 < x
⊢ tan (π / 2 - arcsin x) = sqrt (↑1 - x ^ 2) / x
[PROOFSTEP]
rw_mod_cast [tan_pi_div_two_sub, tan_arcsin, inv_div]
[GOAL]
case refine'_2
x : ℝ
h : 0 < x
⊢ -(π / 2) < π / 2 - arcsin x
[PROOFSTEP]
linarith only [arcsin_le_pi_div_two x, pi_pos]
[GOAL]
case refine'_3
x : ℝ
h : 0 < x
⊢ π / 2 - arcsin x < π / 2
[PROOFSTEP]
linarith only [arcsin_pos.2 h]
