case h
x : ℝ
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
⊢ deriv arcsin = fun x => 1 / sqrt (1 - x ^ 2)
funext x
case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)

case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
case h
x : ℝ
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
by_cases h : x ≠ -1 ∧ x ≠ 1
no goals
case pos
x : ℝ
h : x ≠ -1 ∧ x ≠ 1
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
exact (hasDerivAt_arcsin h.1 h.2).deriv
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / sqrt (1 - x ^ 2)
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ deriv arcsin x = 1 / sqrt (1 - x ^ 2)
rw [deriv_zero_of_not_differentiableAt (mt differentiableAt_arcsin.1 h)]
case neg
x : ℝ
h : x = -1 ∨ x = 1
⊢ 0 = 1 / sqrt (1 - x ^ 2)
case neg
x : ℝ
h : ¬(x ≠ -1 ∧ x ≠ 1)
⊢ 0 = 1 / sqrt (1 - x ^ 2)
simp only [not_and_or, Ne.def, Classical.not_not] at h
no goals
case neg
x : ℝ
h : x = -1 ∨ x = 1
⊢ 0 = 1 / sqrt (1 - x ^ 2)
rcases h with (rfl | rfl) <;> simp