case inl
h : -1 ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - (-1) ^ 2)) (Iic (-1)) (-1)

case inr
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x
x : ℝ
h : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x
rcases em (x = -1) with (rfl | h')
no goals
case inl
h : -1 ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - (-1) ^ 2)) (Iic (-1)) (-1)
convert (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _ <;>
  simp (config := { contextual := true }) [arcsin_of_le_neg_one]
no goals
case inr
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x
exact (hasDerivAt_arcsin h' h).hasDerivWithinAt