case inl
x : ℝ
hx₁ : x ≤ -1
⊢ arcsin (-x) = -arcsin x

case inr
x : ℝ
hx₁ : -1 ≤ x
⊢ arcsin (-x) = -arcsin x
x : ℝ
⊢ arcsin (-x) = -arcsin x
cases' le_total x (-1) with hx₁ hx₁
case inr.inl
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
⊢ arcsin (-x) = -arcsin x

case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x
case inr
x : ℝ
hx₁ : -1 ≤ x
⊢ arcsin (-x) = -arcsin x
cases' le_total 1 x with hx₂ hx₂
case inr.inr.refine'_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x

case inr.inr.refine'_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)
case inr.inr
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ arcsin (-x) = -arcsin x
refine' arcsin_eq_of_sin_eq _ _
no goals
case inl
x : ℝ
hx₁ : x ≤ -1
⊢ arcsin (-x) = -arcsin x
rw [arcsin_of_le_neg_one hx₁, neg_neg, arcsin_of_one_le (le_neg.2 hx₁)]
no goals
case inr.inl
x : ℝ
hx₁ : -1 ≤ x
hx₂ : 1 ≤ x
⊢ arcsin (-x) = -arcsin x
rw [arcsin_of_one_le hx₂, arcsin_of_le_neg_one (neg_le_neg hx₂)]
no goals
case inr.inr.refine'_1
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ sin (-arcsin x) = -x
rw [sin_neg, sin_arcsin hx₁ hx₂]
no goals
case inr.inr.refine'_2
x : ℝ
hx₁ : -1 ≤ x
hx₂ : x ≤ 1
⊢ -arcsin x ∈ Icc (-(π / 2)) (π / 2)
exact ⟨neg_le_neg (arcsin_le_pi_div_two _), neg_le.2 (neg_pi_div_two_le_arcsin _)⟩