[GOAL]
⊢ range arcsin = Icc (-(π / 2)) (π / 2)
[PROOFSTEP]
rw [arcsin, range_comp Subtype.val]
[GOAL]
⊢ Subtype.val '' range (IccExtend arcsin.proof_2 ↑(OrderIso.symm sinOrderIso)) = Icc (-(π / 2)) (π / 2)
[PROOFSTEP]
simp [Icc]
[GOAL]
x : ℝ
⊢ arcsin ↑(projIcc (-1) 1 (_ : -1 ≤ 1) x) = arcsin x
[PROOFSTEP]
rw [arcsin, Function.comp_apply, IccExtend_val, Function.comp_apply, IccExtend, Function.comp_apply]
[GOAL]
x : ℝ
hx : x ∈ Icc (-1) 1
⊢ sin (arcsin x) = x
[PROOFSTEP]
simpa [arcsin, IccExtend_of_mem _ _ hx, -OrderIso.apply_symm_apply] using
  Subtype.ext_iff.1 (sinOrderIso.apply_symm_apply ⟨x, hx⟩)
[GOAL]
x : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
⊢ sin (arcsin (sin x)) = sin x
[PROOFSTEP]
rw [sin_arcsin (neg_one_le_sin _) (sin_le_one _)]
[GOAL]
x y : ℝ
h₁ : sin x = y
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin y = x
[PROOFSTEP]
subst y
[GOAL]
x : ℝ
h₂ : x ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin (sin x) = x
[PROOFSTEP]
exact injOn_sin (arcsin_mem_Icc _) h₂ (sin_arcsin' (sin_mem_Icc x))
[GOAL]
x : ℝ
hx : 1 ≤ x
⊢ arcsin x = π / 2
[PROOFSTEP]
rw [← arcsin_projIcc, projIcc_of_right_le _ hx, Subtype.coe_mk, arcsin_one]
[GOAL]
⊢ sin (-(π / 2)) = -1
[PROOFSTEP]
rw [sin_neg, sin_pi_div_two]
[GOAL]
x : ℝ
hx : x ≤ -1
⊢ arcsin x = -(π / 2)
[PROOFSTEP]
rw [← arcsin_projIcc, projIcc_of_le_left _ hx, Subtype.coe_mk, arcsin_neg_one]
[GOAL]
x : ℝ
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
cases' le_total x (-1) with hx₁ hx₁
[GOAL]
case inl
x : ℝ
hx₁ : x ≤ -1
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]
[GOAL]
case inr
x : ℝ
hx₁ : -1 ≤ x
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
cases' le_total 1 x with hx₂ hx₂
[GOAL]
case inr.inl
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]
[GOAL]
case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x
[PROOFSTEP]
refine' arcsin_eq_of_sin_eq _ _
[GOAL]
case inr.inr.refine'_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x
[PROOFSTEP]
rw [sin_neg, sin_arcsin hx₁ hx₂]
[GOAL]
case inr.inr.refine'_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)
[PROOFSTEP]
exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩
[GOAL]
x y : ℝ
hx : x ∈ Icc (-1) 1
hy : y ∈ Icc (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
rw [← arcsin_sin' hy, strictMonoOn_arcsin.le_iff_le hx (sin_mem_Icc _), arcsin_sin' hy]
[GOAL]
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
cases' le_total x (-1) with hx₁ hx₁
[GOAL]
case inl
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : x ≤ -1
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
simp [arcsin_of_le_neg_one hx₁, hy.1, hx₁.trans (neg_one_le_sin _)]
[GOAL]
case inr
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
cases' lt_or_le 1 x with hx₂ hx₂
[GOAL]
case inr.inl
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
simp [arcsin_of_one_le hx₂.le, hy.2.not_le, (sin_le_one y).trans_lt hx₂]
[GOAL]
case inr.inr
x y : ℝ
hy : y ∈ Ico (-(π / 2)) (π / 2)
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin x ≤ y ↔ x ≤ sin y
[PROOFSTEP]
exact arcsin_le_iff_le_sin ⟨hx₁, hx₂⟩ (mem_Icc_of_Ico hy)
[GOAL]
x y : ℝ
hx : x ∈ Icc (-(π / 2)) (π / 2)
hy : y ∈ Icc (-1) 1
⊢ x ≤ arcsin y ↔ sin x ≤ y
[PROOFSTEP]
rw [← neg_le_neg_iff, ← arcsin_neg,
  arcsin_le_iff_le_sin ⟨neg_le_neg hy.2, neg_le.2 hy.1⟩ ⟨neg_le_neg hx.2, neg_le.2 hx.1⟩, sin_neg, neg_le_neg_iff]
[GOAL]
x y : ℝ
hx : x ∈ Ioc (-(π / 2)) (π / 2)
⊢ x ≤ arcsin y ↔ sin x ≤ y
[PROOFSTEP]
rw [← neg_le_neg_iff, ← arcsin_neg, arcsin_le_iff_le_sin' ⟨neg_le_neg hx.2, neg_lt.2 hx.1⟩, sin_neg, neg_le_neg_iff]
[GOAL]
x y : ℝ
hy : y ∈ Ioo (-(π / 2)) (π / 2)
⊢ arcsin x = y ↔ x = sin y
[PROOFSTEP]
simp only [le_antisymm_iff, arcsin_le_iff_le_sin' (mem_Ico_of_Ioo hy), le_arcsin_iff_sin_le' (mem_Ioc_of_Ioo hy)]
[GOAL]
x : ℝ
⊢ sin 0 ≤ x ↔ 0 ≤ x
[PROOFSTEP]
rw [sin_zero]
[GOAL]
x : ℝ
⊢ arcsin x = 0 ↔ x = 0
[PROOFSTEP]
simp [le_antisymm_iff]
[GOAL]
x : ℝ
⊢ x < sin (π / 2) ↔ x < 1
[PROOFSTEP]
rw [sin_pi_div_two]
[GOAL]
x : ℝ
⊢ sin (-(π / 2)) < x ↔ -1 < x
[PROOFSTEP]
rw [sin_neg, sin_pi_div_two]
[GOAL]
x : ℝ
⊢ π / 4 ≤ arcsin x ↔ sqrt 2 / 2 ≤ x
[PROOFSTEP]
rw [← sin_pi_div_four, le_arcsin_iff_sin_le']
[GOAL]
x : ℝ
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
[PROOFSTEP]
have := pi_pos
[GOAL]
x : ℝ
this : 0 < π
⊢ π / 4 ∈ Ioc (-(π / 2)) (π / 2)
[PROOFSTEP]
constructor
[GOAL]
case left
x : ℝ
this : 0 < π
⊢ -(π / 2) < π / 4
[PROOFSTEP]
linarith
[GOAL]
case right
x : ℝ
this : 0 < π
⊢ π / 4 ≤ π / 2
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
h : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ sin x ∈ Ioo (-1) 1
[PROOFSTEP]
rwa [mem_Ioo, ← arcsin_lt_pi_div_two, ← neg_pi_div_two_lt_arcsin, arcsin_sin h.1.le h.2.le]
[GOAL]
x : ℝ
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₁ : -1 ≤ x
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : ¬-1 ≤ x ⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [not_le] at hx₁ 
[GOAL]
case neg
x : ℝ
hx₁ : x < -1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
[GOAL]
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₂ : x ≤ 1
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : -1 ≤ x hx₂ : ¬x ≤ 1 ⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [not_le] at hx₂ 
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
have : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1 := sin_sq_add_cos_sq (arcsin x)
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [← eq_sub_iff_add_eq', ← sqrt_inj (sq_nonneg _) (sub_nonneg.2 (sin_sq_le_one (arcsin x))), sq,
  sqrt_mul_self (cos_arcsin_nonneg _)] at this 
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
this : cos (arcsin x) = sqrt (1 - sin (arcsin x) ^ 2)
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [this, sin_arcsin hx₁ hx₂]
[GOAL]
x : ℝ
⊢ tan (arcsin x) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [tan_eq_sin_div_cos, cos_arcsin]
[GOAL]
x : ℝ
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₁ : -1 ≤ x
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : ¬-1 ≤ x ⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
have h : sqrt (1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
[GOAL]
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [h]
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
[PROOFSTEP]
simp
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₂ : x ≤ 1
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : -1 ≤ x hx₂ : ¬x ≤ 1 ⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
have h : sqrt (1 - x ^ 2) = 0 := sqrt_eq_zero_of_nonpos (by nlinarith)
[GOAL]
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [h]
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
h : sqrt (1 - x ^ 2) = 0
⊢ sin (arcsin x) / 0 = x / 0
[PROOFSTEP]
simp
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arcsin x) / sqrt (1 - x ^ 2) = x / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [sin_arcsin hx₁ hx₂]
[GOAL]
x : ℝ
⊢ arcsin x = π / 2 - arccos x
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
⊢ arccos x ≤ π
[PROOFSTEP]
unfold arccos
[GOAL]
x : ℝ
⊢ π / 2 - arcsin x ≤ π
[PROOFSTEP]
linarith [neg_pi_div_two_le_arcsin x]
[GOAL]
x : ℝ
⊢ 0 ≤ arccos x
[PROOFSTEP]
unfold arccos
[GOAL]
x : ℝ
⊢ 0 ≤ π / 2 - arcsin x
[PROOFSTEP]
linarith [arcsin_le_pi_div_two x]
[GOAL]
x : ℝ
⊢ 0 < arccos x ↔ x < 1
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arccos x) = x
[PROOFSTEP]
rw [arccos, cos_pi_div_two_sub, sin_arcsin hx₁ hx₂]
[GOAL]
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ arccos (cos x) = x
[PROOFSTEP]
rw [arccos, ← sin_pi_div_two_sub, arcsin_sin]
[GOAL]
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - (π / 2 - x) = x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ -(π / 2) ≤ π / 2 - x
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ π / 2 - x ≤ π / 2
[PROOFSTEP]
simp [sub_eq_add_neg]
[GOAL]
case hx₁
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ x ≤ π
[PROOFSTEP]
linarith
[GOAL]
case hx₂
x : ℝ
hx₁ : 0 ≤ x
hx₂ : x ≤ π
⊢ 0 ≤ x
[PROOFSTEP]
linarith
[GOAL]
⊢ arccos 0 = π / 2
[PROOFSTEP]
simp [arccos]
[GOAL]
⊢ arccos 1 = 0
[PROOFSTEP]
simp [arccos]
[GOAL]
⊢ arccos (-1) = π
[PROOFSTEP]
simp [arccos, add_halves]
[GOAL]
x : ℝ
⊢ arccos x = 0 ↔ 1 ≤ x
[PROOFSTEP]
simp [arccos, sub_eq_zero]
[GOAL]
x : ℝ
⊢ arccos x = π / 2 ↔ x = 0
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
⊢ arccos x = π ↔ x ≤ -1
[PROOFSTEP]
rw [arccos, sub_eq_iff_eq_add, ← sub_eq_iff_eq_add', div_two_sub_self, neg_pi_div_two_eq_arcsin]
[GOAL]
x : ℝ
⊢ arccos (-x) = π - arccos x
[PROOFSTEP]
rw [← add_halves π, arccos, arcsin_neg, arccos, add_sub_assoc, sub_sub_self, sub_neg_eq_add]
[GOAL]
x : ℝ
hx : 1 ≤ x
⊢ arccos x = 0
[PROOFSTEP]
rw [arccos, arcsin_of_one_le hx, sub_self]
[GOAL]
x : ℝ
hx : x ≤ -1
⊢ arccos x = π
[PROOFSTEP]
rw [arccos, arcsin_of_le_neg_one hx, sub_neg_eq_add, add_halves']
[GOAL]
x : ℝ
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₁ : -1 ≤ x
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : ¬-1 ≤ x ⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [not_le] at hx₁ 
[GOAL]
case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
[GOAL]
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases hx₂ : x ≤ 1
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
case neg x : ℝ hx₁ : -1 ≤ x hx₂ : ¬x ≤ 1 ⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
swap
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [not_le] at hx₂ 
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
[GOAL]
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
[PROOFSTEP]
nlinarith
[GOAL]
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]
[GOAL]
x : ℝ
⊢ arccos x ≤ π / 2 ↔ 0 ≤ x
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
⊢ arccos x < π / 2 ↔ 0 < x
[PROOFSTEP]
simp [arccos]
[GOAL]
x : ℝ
⊢ arccos x ≤ π / 4 ↔ sqrt 2 / 2 ≤ x
[PROOFSTEP]
rw [arccos, ← pi_div_four_le_arcsin]
[GOAL]
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 ↔ π / 4 ≤ arcsin x
[PROOFSTEP]
constructor
[GOAL]
case mp
x : ℝ
⊢ π / 2 - arcsin x ≤ π / 4 → π / 4 ≤ arcsin x
[PROOFSTEP]
intro
[GOAL]
case mp
x : ℝ
a✝ : π / 2 - arcsin x ≤ π / 4
⊢ π / 4 ≤ arcsin x
[PROOFSTEP]
linarith
[GOAL]
case mpr
x : ℝ
⊢ π / 4 ≤ arcsin x → π / 2 - arcsin x ≤ π / 4
[PROOFSTEP]
intro
[GOAL]
case mpr
x : ℝ
a✝ : π / 4 ≤ arcsin x
⊢ π / 2 - arcsin x ≤ π / 4
[PROOFSTEP]
linarith
[GOAL]
x : ℝ
⊢ tan (arccos x) = sqrt (1 - x ^ 2) / x
[PROOFSTEP]
rw [arccos, tan_pi_div_two_sub, tan_arcsin, inv_div]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ 2
[PROOFSTEP]
norm_num
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arcsin x = arccos (sqrt (1 - x ^ 2))
[PROOFSTEP]
rw [eq_comm, ← cos_arcsin]
[GOAL]
x : ℝ
h : 0 ≤ x
⊢ arccos (cos (arcsin x)) = arcsin x
[PROOFSTEP]
exact arccos_cos (arcsin_nonneg.2 h) ((arcsin_le_pi_div_two _).trans (div_le_self pi_pos.le one_le_two))
