Derivative cannot simp

Stream: mathlib4

[Jiatong Yang]

Mathlib.Analysis.Calculus.Deriv.Basic says that we can use "simp" to simplify the derviative of simple functions, but it's not the case.

import Mathlib
open Real

example (x : ℝ) : deriv (λ x => cos x + 2 * sin x) x = -sin x + 2 * cos x := by
  simp

[Yury G. Kudryashov]

AFAICT, this was the case in Lean 3 but got lost during the port, I'm not sure why. It would be nice if someone investigates why this happens. E.g., you can try to prove Differentiable for both terms by simp, then find the simplest that fails.

[Patrick Massot]

Yes, porting the differential calculus chapter of MIL was a pain because of this. I had to remove a lot of nice examples. But @Tomas Skrivan’s tactics were meant to be a better replacement anyway.

[Jiatong Yang]

Patrick Massot said:

Yes, porting the differential calculus chapter of MIL was a pain because of this. I had to remove a lot of nice examples. But Tomas Skrivan’s tactics were meant to be a better replacement anyway.

I'm sorry, but where can I see Tomas Skrivan’s tactics?

[Patrick Massot]

In the SciLean project.

[Floris van Doorn]

We can easily get this behavior back by tagging a few more lemmas with @[simp]:

import Mathlib
open Real

attribute [simp] differentiableAt_sin differentiableAt_cos

example (x : ℝ) : deriv (λ x => cos x + 2 * sin x) x = -sin x + 2 * cos x := by
  simp

[Floris van Doorn]

#18874

[Patrick Massot]

Yes, I wanted to say there is also hope that things got better with simp. The MIL port was very early and simp got a lot of work since then.