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

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