case hderiv
a b : ℝ
n : ℕ
⊢ deriv sin = fun x => cos x

case hdiff
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ sin x

case hcont
a b : ℝ
n : ℕ
⊢ ContinuousOn (fun x => cos x) [[a, b]]
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x) = sin b - sin a
rw [integral_deriv_eq_sub']
no goals
case hderiv
a b : ℝ
n : ℕ
⊢ deriv sin = fun x => cos x
norm_num
no goals
case hdiff
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ sin x
simp only [differentiableAt_sin, implies_true]
no goals
case hcont
a b : ℝ
n : ℕ
⊢ ContinuousOn (fun x => cos x) [[a, b]]
exact continuousOn_cos