x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ x ≠ 1
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1
refine' ⟨fun h => _, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ x ≠ 1
rw [← neg_neg x, ← image_neg_Ici] at h
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
this : DifferentiableWithinAt ℝ (fun y => -(arcsin ∘ Neg.neg) y) (Ici (-x)) (-x)
⊢ x ≠ 1
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1
have := (h.comp (-x) differentiableWithinAt_id.neg (mapsTo_image _ _)).neg