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)
x : ℝ
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
by_cases hx₁ : -1 ≤ x
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)

case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
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)
swap
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)
case pos
x : ℝ
hx₁ : -1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
by_cases hx₂ : x ≤ 1
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)

case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
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)
swap
no goals
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
rw [arccos_eq_pi_div_two_sub_arcsin, sin_pi_div_two_sub, cos_arcsin]
case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
rw [not_le] at hx₁
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0
case neg
x : ℝ
hx₁ : x < -1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
rw [arccos_of_le_neg_one hx₁.le, sin_pi, sqrt_eq_zero_of_nonpos]
no goals
case neg
x : ℝ
hx₁ : x < -1
⊢ 1 - x ^ 2 ≤ 0
nlinarith
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
rw [not_le] at hx₂
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ sin (arccos x) = sqrt (1 - x ^ 2)
rw [arccos_of_one_le hx₂.le, sin_zero, sqrt_eq_zero_of_nonpos]
no goals
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
nlinarith