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

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

case hcont
a b : ℝ
n : ℕ
⊢ ContinuousOn (fun x => exp x) [[a, b]]
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, exp x) = exp b - exp a
rw [integral_deriv_eq_sub']
no goals
case hderiv
a b : ℝ
n : ℕ
⊢ deriv exp = fun x => exp x
norm_num
no goals
case hdiff
a b : ℝ
n : ℕ
⊢ ∀ (x : ℝ), x ∈ [[a, b]] → DifferentiableAt ℝ exp x
exact fun _ _ => differentiableAt_exp
no goals
case hcont
a b : ℝ
n : ℕ
⊢ ContinuousOn (fun x => exp x) [[a, b]]
exact continuousOn_exp