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

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

case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
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)
swap
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)
case pos
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
have : sin (arcsin x) ^ 2 + cos (arcsin x) ^ 2 = 1 := sin_sq_add_cos_sq (arcsin x)
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)
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)
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
no goals
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)
rw [this, sin_arcsin hx₁ hx₂]
case neg
x : ℝ
hx₁ : x < -1
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
case neg
x : ℝ
hx₁ : ¬-1 ≤ x
⊢ cos (arcsin 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
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
rw [arcsin_of_le_neg_one hx₁.le, cos_neg, cos_pi_div_two, 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
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : ¬x ≤ 1
⊢ cos (arcsin 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
⊢ cos (arcsin x) = sqrt (1 - x ^ 2)
rw [arcsin_of_one_le hx₂.le, cos_pi_div_two, sqrt_eq_zero_of_nonpos]
no goals
case neg
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 < x
⊢ 1 - x ^ 2 ≤ 0
nlinarith