[GOAL]
x : ℝ
h₁ : x ≠ -1
h₂ : x ≠ 1
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
cases' h₁.lt_or_lt with h₁ h₁
[GOAL]
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : 1 - x ^ 2 < 0 := by nlinarith [h₁]
[GOAL]
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
⊢ 1 - x ^ 2 < 0
[PROOFSTEP]
nlinarith [h₁]
[GOAL]
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
rw [sqrt_eq_zero'.2 this.le, div_zero]
[GOAL]
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : arcsin =ᶠ[𝓝 x] fun _ => -(π / 2) := (gt_mem_nhds h₁).mono fun y hy => arcsin_of_le_neg_one hy.le
[GOAL]
case inl
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : x < -1
this✝ : 1 - x ^ 2 < 0
this : arcsin =ᶠ[𝓝 x] fun x => -(π / 2)
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
exact ⟨(hasStrictDerivAt_const _ _).congr_of_eventuallyEq this.symm, contDiffAt_const.congr_of_eventuallyEq this⟩
[GOAL]
case inr
x : ℝ
h₁✝ : x ≠ -1
h₂ : x ≠ 1
h₁ : -1 < x
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
cases' h₂.lt_or_lt with h₂ h₂
[GOAL]
case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : 0 < sqrt (1 - x ^ 2) := sqrt_pos.2 (by nlinarith [h₁, h₂])
[GOAL]
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
⊢ 0 < 1 - x ^ 2
[PROOFSTEP]
nlinarith [h₁, h₂]
[GOAL]
case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < sqrt (1 - x ^ 2)
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
simp only [← cos_arcsin, one_div] at this ⊢
[GOAL]
case inr.inl
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : x < 1
this : 0 < cos (arcsin x)
⊢ HasStrictDerivAt arcsin (cos (arcsin x))⁻¹ x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
exact
  ⟨sinLocalHomeomorph.hasStrictDerivAt_symm ⟨h₁, h₂⟩ this.ne' (hasStrictDerivAt_sin _),
    sinLocalHomeomorph.contDiffAt_symm_deriv this.ne' ⟨h₁, h₂⟩ (hasDerivAt_sin _) contDiff_sin.contDiffAt⟩
[GOAL]
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : 1 - x ^ 2 < 0 := by nlinarith [h₂]
[GOAL]
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
⊢ 1 - x ^ 2 < 0
[PROOFSTEP]
nlinarith [h₂]
[GOAL]
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin (1 / sqrt (1 - x ^ 2)) x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
rw [sqrt_eq_zero'.2 this.le, div_zero]
[GOAL]
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this : 1 - x ^ 2 < 0
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
have : arcsin =ᶠ[𝓝 x] fun _ => π / 2 := (lt_mem_nhds h₂).mono fun y hy => arcsin_of_one_le hy.le
[GOAL]
case inr.inr
x : ℝ
h₁✝ : x ≠ -1
h₂✝ : x ≠ 1
h₁ : -1 < x
h₂ : 1 < x
this✝ : 1 - x ^ 2 < 0
this : arcsin =ᶠ[𝓝 x] fun x => π / 2
⊢ HasStrictDerivAt arcsin 0 x ∧ ContDiffAt ℝ ⊤ arcsin x
[PROOFSTEP]
exact ⟨(hasStrictDerivAt_const _ _).congr_of_eventuallyEq this.symm, contDiffAt_const.congr_of_eventuallyEq this⟩
[GOAL]
x : ℝ
h : x ≠ -1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Ici x) x
[PROOFSTEP]
rcases eq_or_ne x 1 with (rfl | h')
[GOAL]
case inl
h : 1 ≠ -1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - 1 ^ 2)) (Ici 1) 1
[PROOFSTEP]
convert (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _
[GOAL]
case h.e'_7
h : 1 ≠ -1
⊢ 1 / sqrt (1 - 1 ^ 2) = 0
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_one_le]
[GOAL]
case inl.convert_3
h : 1 ≠ -1
⊢ ∀ (x : ℝ), x ∈ Ici 1 → arcsin x = π / 2
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_one_le]
[GOAL]
case inl.convert_4
h : 1 ≠ -1
⊢ arcsin 1 = π / 2
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_one_le]
[GOAL]
case inr
x : ℝ
h : x ≠ -1
h' : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Ici x) x
[PROOFSTEP]
exact (hasDerivAt_arcsin h h').hasDerivWithinAt
[GOAL]
x : ℝ
h : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x
[PROOFSTEP]
rcases em (x = -1) with (rfl | h')
[GOAL]
case inl
h : -1 ≠ 1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - (-1) ^ 2)) (Iic (-1)) (-1)
[PROOFSTEP]
convert (hasDerivWithinAt_const (-1 : ℝ) _ (-(π / 2))).congr _ _
[GOAL]
case h.e'_7
h : -1 ≠ 1
⊢ 1 / sqrt (1 - (-1) ^ 2) = 0
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_le_neg_one]
[GOAL]
case inl.convert_3
h : -1 ≠ 1
⊢ ∀ (x : ℝ), x ∈ Iic (-1) → arcsin x = -(π / 2)
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_le_neg_one]
[GOAL]
case inl.convert_4
h : -1 ≠ 1
⊢ arcsin (-1) = -(π / 2)
[PROOFSTEP]
simp (config := { contextual := true }) [arcsin_of_le_neg_one]
[GOAL]
case inr
x : ℝ
h : x ≠ 1
h' : ¬x = -1
⊢ HasDerivWithinAt arcsin (1 / sqrt (1 - x ^ 2)) (Iic x) x
[PROOFSTEP]
exact (hasDerivAt_arcsin h' h).hasDerivWithinAt
[GOAL]
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x ↔ x ≠ -1
[PROOFSTEP]
refine' ⟨_, fun h => (hasDerivWithinAt_arcsin_Ici h).differentiableWithinAt⟩
[GOAL]
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Ici x) x → x ≠ -1
[PROOFSTEP]
rintro h rfl
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ False
[PROOFSTEP]
have : sin ∘ arcsin =ᶠ[𝓝[≥] (-1 : ℝ)] id := by
  filter_upwards [Icc_mem_nhdsWithin_Ici ⟨le_rfl, neg_lt_self (zero_lt_one' ℝ)⟩] with x using sin_arcsin'
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
⊢ sin ∘ arcsin =ᶠ[𝓝[Ici (-1)] (-1)] id
[PROOFSTEP]
filter_upwards [Icc_mem_nhdsWithin_Ici ⟨le_rfl, neg_lt_self (zero_lt_one' ℝ)⟩] with x using sin_arcsin'
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[Ici (-1)] (-1)] id
⊢ False
[PROOFSTEP]
have := h.hasDerivWithinAt.sin.congr_of_eventuallyEq this.symm (by simp)
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this : sin ∘ arcsin =ᶠ[𝓝[Ici (-1)] (-1)] id
⊢ id (-1) = sin (arcsin (-1))
[PROOFSTEP]
simp
[GOAL]
h : DifferentiableWithinAt ℝ arcsin (Ici (-1)) (-1)
this✝ : sin ∘ arcsin =ᶠ[𝓝[Ici (-1)] (-1)] id
this : HasDerivWithinAt id (cos (arcsin (-1)) * derivWithin arcsin (Ici (-1)) (-1)) (Ici (-1)) (-1)
⊢ False
[PROOFSTEP]
simpa using (uniqueDiffOn_Ici _ _ left_mem_Ici).eq_deriv _ this (hasDerivWithinAt_id _ _)
[GOAL]
x : ℝ
⊢ DifferentiableWithinAt ℝ arcsin (Iic x) x ↔ x ≠ 1
[PROOFSTEP]
refine' ⟨fun h => _, fun h => (hasDerivWithinAt_arcsin_Iic h).differentiableWithinAt⟩
[GOAL]
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Iic x) x
⊢ x ≠ 1
[PROOFSTEP]
rw [← neg_neg x, ← image_neg_Ici] at h 
[GOAL]
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
⊢ x ≠ 1
[PROOFSTEP]
have := (h.comp (-x) differentiableWithinAt_id.neg (mapsTo_image _ _)).neg
[GOAL]
x : ℝ
h : DifferentiableWithinAt ℝ arcsin (Neg.neg '' Ici (-x)) (- -x)
this : DifferentiableWithinAt ℝ (fun y => -(arcsin ∘ Neg.neg) y) (Ici (-x)) (-x)
⊢ x ≠ 1
[PROOFSTEP]
simpa [(· ∘ ·), differentiableWithinAt_arcsin_Ici] using this
[GOAL]
⊢ deriv arcsin = fun x => 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
funext x
[GOAL]
case h
x : ℝ
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
by_cases h : x ≠ -1 ∧ x ≠ 1
[GOAL]
case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
exact (hasDerivAt_arcsin h.1 h.2).deriv
[GOAL]
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
[GOAL]
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
simp only [not_and_or, Ne.def, Classical.not_not] at h 
[GOAL]
case neg
x : ℝ
h : x = -1 ∨ x = 1
⊢ 0 = 1 / sqrt (1 - x ^ 2)
[PROOFSTEP]
rcases h with (rfl | rfl)
[GOAL]
case neg.inl
⊢ 0 = 1 / sqrt (1 - (-1) ^ 2)
[PROOFSTEP]
simp
[GOAL]
case neg.inr
⊢ 0 = 1 / sqrt (1 - 1 ^ 2)
[PROOFSTEP]
simp
[GOAL]
x : ℝ
⊢ -deriv (fun y => arcsin y) x = -(1 / sqrt (1 - x ^ 2))
[PROOFSTEP]
simp only [deriv_arcsin]
[GOAL]
x : ℝ
n : ℕ∞
⊢ ContDiffAt ℝ n arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
[PROOFSTEP]
refine' Iff.trans ⟨fun h => _, fun h => _⟩ contDiffAt_arcsin_iff
[GOAL]
case refine'_1
x : ℝ
n : ℕ∞
h : ContDiffAt ℝ n arccos x
⊢ ContDiffAt ℝ n arcsin x
[PROOFSTEP]
simpa [arccos] using (@contDiffAt_const _ _ _ _ _ _ _ _ _ _ (π / 2)).sub h
[GOAL]
case refine'_2
x : ℝ
n : ℕ∞
h : ContDiffAt ℝ n arcsin x
⊢ ContDiffAt ℝ n arccos x
[PROOFSTEP]
simpa [arccos] using (@contDiffAt_const _ _ _ _ _ _ _ _ _ _ (π / 2)).sub h
