a b : ℝ
n : ℕ
⊢ -cos b - -cos a = cos a - cos b

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

case hdiff
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ (fun x => -cos x) x

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