chore: add some simp and fun_prop attributes (#18874)

* Also add a test file that uses the `simp` lemmas.
* Add/move the `fun_prop` lemmas to the compositional lemmas.

[Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Derivative.20cannot.20simp)

Mathlib/Analysis/Calculus/Deriv/Basic.lean

@@ -68,7 +68,7 @@ and they more frequently lead to the desired result.
 We set up the simplifier so that it can compute the derivative of simple functions. For instance,
 ```lean
 example (x : ℝ) :
-    deriv (fun x ↦ cos (sin x) * exp x) x = (cos(sin(x))-sin(sin(x))*cos(x))*exp(x) := by
+    deriv (fun x ↦ cos (sin x) * exp x) x = (cos (sin x) - sin (sin x) * cos x) * exp x := by
   simp; ring
 ```
 

Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean

@@ -73,9 +73,11 @@ theorem hasDerivAt_exp (x : ℂ) : HasDerivAt exp (exp x) x := by
   simp only [Metric.mem_ball, dist_zero_right, norm_pow]
   exact fun z hz => exp_bound_sq x z hz.le
 
+@[simp]
 theorem differentiable_exp : Differentiable 𝕜 exp := fun x =>
   (hasDerivAt_exp x).differentiableAt.restrictScalars 𝕜
 
+@[simp]
 theorem differentiableAt_exp {x : ℂ} : DifferentiableAt 𝕜 exp x :=
   differentiable_exp x
 
@@ -148,15 +150,15 @@ theorem DifferentiableWithinAt.cexp (hf : DifferentiableWithinAt 𝕜 f s x) :
     DifferentiableWithinAt 𝕜 (fun x => Complex.exp (f x)) s x :=
   hf.hasFDerivWithinAt.cexp.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.cexp (hc : DifferentiableAt 𝕜 f x) :
     DifferentiableAt 𝕜 (fun x => Complex.exp (f x)) x :=
   hc.hasFDerivAt.cexp.differentiableAt
 
 theorem DifferentiableOn.cexp (hc : DifferentiableOn 𝕜 f s) :
     DifferentiableOn 𝕜 (fun x => Complex.exp (f x)) s := fun x h => (hc x h).cexp
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.cexp (hc : Differentiable 𝕜 f) :
     Differentiable 𝕜 fun x => Complex.exp (f x) := fun x => (hc x).cexp
 
@@ -231,8 +233,10 @@ theorem hasDerivAt_exp (x : ℝ) : HasDerivAt exp (exp x) x :=
 theorem contDiff_exp {n : ℕ∞} : ContDiff ℝ n exp :=
   Complex.contDiff_exp.real_of_complex
 
+@[simp]
 theorem differentiable_exp : Differentiable ℝ exp := fun x => (hasDerivAt_exp x).differentiableAt
 
+@[simp]
 theorem differentiableAt_exp {x : ℝ} : DifferentiableAt ℝ exp x :=
   differentiable_exp x
 
@@ -316,15 +320,15 @@ theorem DifferentiableWithinAt.exp (hf : DifferentiableWithinAt ℝ f s x) :
     DifferentiableWithinAt ℝ (fun x => Real.exp (f x)) s x :=
   hf.hasFDerivWithinAt.exp.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.exp (hc : DifferentiableAt ℝ f x) :
     DifferentiableAt ℝ (fun x => Real.exp (f x)) x :=
   hc.hasFDerivAt.exp.differentiableAt
 
 theorem DifferentiableOn.exp (hc : DifferentiableOn ℝ f s) :
     DifferentiableOn ℝ (fun x => Real.exp (f x)) s := fun x h => (hc x h).exp
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.exp (hc : Differentiable ℝ f) : Differentiable ℝ fun x => Real.exp (f x) :=
   fun x => (hc x).exp
 

Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

@@ -45,10 +45,10 @@ theorem contDiff_sin {n} : ContDiff ℂ n sin :=
   (((contDiff_neg.mul contDiff_const).cexp.sub (contDiff_id.mul contDiff_const).cexp).mul
     contDiff_const).div_const _
 
-@[fun_prop]
+@[simp]
 theorem differentiable_sin : Differentiable ℂ sin := fun x => (hasDerivAt_sin x).differentiableAt
 
-@[fun_prop]
+@[simp]
 theorem differentiableAt_sin {x : ℂ} : DifferentiableAt ℂ sin x :=
   differentiable_sin x
 
@@ -72,10 +72,10 @@ theorem hasDerivAt_cos (x : ℂ) : HasDerivAt cos (-sin x) x :=
 theorem contDiff_cos {n} : ContDiff ℂ n cos :=
   ((contDiff_id.mul contDiff_const).cexp.add (contDiff_neg.mul contDiff_const).cexp).div_const _
 
-@[fun_prop]
+@[simp]
 theorem differentiable_cos : Differentiable ℂ cos := fun x => (hasDerivAt_cos x).differentiableAt
 
-@[fun_prop]
+@[simp]
 theorem differentiableAt_cos {x : ℂ} : DifferentiableAt ℂ cos x :=
   differentiable_cos x
 
@@ -102,10 +102,10 @@ theorem hasDerivAt_sinh (x : ℂ) : HasDerivAt sinh (cosh x) x :=
 theorem contDiff_sinh {n} : ContDiff ℂ n sinh :=
   (contDiff_exp.sub contDiff_neg.cexp).div_const _
 
-@[fun_prop]
+@[simp]
 theorem differentiable_sinh : Differentiable ℂ sinh := fun x => (hasDerivAt_sinh x).differentiableAt
 
-@[fun_prop]
+@[simp]
 theorem differentiableAt_sinh {x : ℂ} : DifferentiableAt ℂ sinh x :=
   differentiable_sinh x
 
@@ -129,10 +129,10 @@ theorem hasDerivAt_cosh (x : ℂ) : HasDerivAt cosh (sinh x) x :=
 theorem contDiff_cosh {n} : ContDiff ℂ n cosh :=
   (contDiff_exp.add contDiff_neg.cexp).div_const _
 
-@[fun_prop]
+@[simp]
 theorem differentiable_cosh : Differentiable ℂ cosh := fun x => (hasDerivAt_cosh x).differentiableAt
 
-@[fun_prop]
+@[simp]
 theorem differentiableAt_cosh {x : ℂ} : DifferentiableAt ℂ cosh x :=
   differentiable_cosh x
 
@@ -274,15 +274,15 @@ theorem DifferentiableWithinAt.ccos (hf : DifferentiableWithinAt ℂ f s x) :
     DifferentiableWithinAt ℂ (fun x => Complex.cos (f x)) s x :=
   hf.hasFDerivWithinAt.ccos.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.ccos (hc : DifferentiableAt ℂ f x) :
     DifferentiableAt ℂ (fun x => Complex.cos (f x)) x :=
   hc.hasFDerivAt.ccos.differentiableAt
 
 theorem DifferentiableOn.ccos (hc : DifferentiableOn ℂ f s) :
     DifferentiableOn ℂ (fun x => Complex.cos (f x)) s := fun x h => (hc x h).ccos
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.ccos (hc : Differentiable ℂ f) :
     Differentiable ℂ fun x => Complex.cos (f x) := fun x => (hc x).ccos
 
@@ -329,15 +329,15 @@ theorem DifferentiableWithinAt.csin (hf : DifferentiableWithinAt ℂ f s x) :
     DifferentiableWithinAt ℂ (fun x => Complex.sin (f x)) s x :=
   hf.hasFDerivWithinAt.csin.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.csin (hc : DifferentiableAt ℂ f x) :
     DifferentiableAt ℂ (fun x => Complex.sin (f x)) x :=
   hc.hasFDerivAt.csin.differentiableAt
 
 theorem DifferentiableOn.csin (hc : DifferentiableOn ℂ f s) :
     DifferentiableOn ℂ (fun x => Complex.sin (f x)) s := fun x h => (hc x h).csin
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.csin (hc : Differentiable ℂ f) :
     Differentiable ℂ fun x => Complex.sin (f x) := fun x => (hc x).csin
 
@@ -384,15 +384,15 @@ theorem DifferentiableWithinAt.ccosh (hf : DifferentiableWithinAt ℂ f s x) :
     DifferentiableWithinAt ℂ (fun x => Complex.cosh (f x)) s x :=
   hf.hasFDerivWithinAt.ccosh.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.ccosh (hc : DifferentiableAt ℂ f x) :
     DifferentiableAt ℂ (fun x => Complex.cosh (f x)) x :=
   hc.hasFDerivAt.ccosh.differentiableAt
 
 theorem DifferentiableOn.ccosh (hc : DifferentiableOn ℂ f s) :
     DifferentiableOn ℂ (fun x => Complex.cosh (f x)) s := fun x h => (hc x h).ccosh
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.ccosh (hc : Differentiable ℂ f) :
     Differentiable ℂ fun x => Complex.cosh (f x) := fun x => (hc x).ccosh
 
@@ -439,15 +439,15 @@ theorem DifferentiableWithinAt.csinh (hf : DifferentiableWithinAt ℂ f s x) :
     DifferentiableWithinAt ℂ (fun x => Complex.sinh (f x)) s x :=
   hf.hasFDerivWithinAt.csinh.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.csinh (hc : DifferentiableAt ℂ f x) :
     DifferentiableAt ℂ (fun x => Complex.sinh (f x)) x :=
   hc.hasFDerivAt.csinh.differentiableAt
 
 theorem DifferentiableOn.csinh (hc : DifferentiableOn ℂ f s) :
     DifferentiableOn ℂ (fun x => Complex.sinh (f x)) s := fun x h => (hc x h).csinh
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.csinh (hc : Differentiable ℂ f) :
     Differentiable ℂ fun x => Complex.sinh (f x) := fun x => (hc x).csinh
 
@@ -490,10 +490,10 @@ theorem hasDerivAt_sin (x : ℝ) : HasDerivAt sin (cos x) x :=
 theorem contDiff_sin {n} : ContDiff ℝ n sin :=
   Complex.contDiff_sin.real_of_complex
 
-@[fun_prop]
+@[simp]
 theorem differentiable_sin : Differentiable ℝ sin := fun x => (hasDerivAt_sin x).differentiableAt
 
-@[fun_prop]
+@[simp]
 theorem differentiableAt_sin : DifferentiableAt ℝ sin x :=
   differentiable_sin x
 
@@ -510,10 +510,10 @@ theorem hasDerivAt_cos (x : ℝ) : HasDerivAt cos (-sin x) x :=
 theorem contDiff_cos {n} : ContDiff ℝ n cos :=
   Complex.contDiff_cos.real_of_complex
 
-@[fun_prop]
+@[simp]
 theorem differentiable_cos : Differentiable ℝ cos := fun x => (hasDerivAt_cos x).differentiableAt
 
-@[fun_prop]
+@[simp]
 theorem differentiableAt_cos : DifferentiableAt ℝ cos x :=
   differentiable_cos x
 
@@ -533,10 +533,10 @@ theorem hasDerivAt_sinh (x : ℝ) : HasDerivAt sinh (cosh x) x :=
 theorem contDiff_sinh {n} : ContDiff ℝ n sinh :=
   Complex.contDiff_sinh.real_of_complex
 
-@[fun_prop]
+@[simp]
 theorem differentiable_sinh : Differentiable ℝ sinh := fun x => (hasDerivAt_sinh x).differentiableAt
 
-@[fun_prop]
+@[simp]
 theorem differentiableAt_sinh : DifferentiableAt ℝ sinh x :=
   differentiable_sinh x
 
@@ -553,10 +553,10 @@ theorem hasDerivAt_cosh (x : ℝ) : HasDerivAt cosh (sinh x) x :=
 theorem contDiff_cosh {n} : ContDiff ℝ n cosh :=
   Complex.contDiff_cosh.real_of_complex
 
-@[fun_prop]
+@[simp]
 theorem differentiable_cosh : Differentiable ℝ cosh := fun x => (hasDerivAt_cosh x).differentiableAt
 
-@[fun_prop]
+@[simp]
 theorem differentiableAt_cosh : DifferentiableAt ℝ cosh x :=
   differentiable_cosh x
 
@@ -786,15 +786,15 @@ theorem DifferentiableWithinAt.cos (hf : DifferentiableWithinAt ℝ f s x) :
     DifferentiableWithinAt ℝ (fun x => Real.cos (f x)) s x :=
   hf.hasFDerivWithinAt.cos.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.cos (hc : DifferentiableAt ℝ f x) :
     DifferentiableAt ℝ (fun x => Real.cos (f x)) x :=
   hc.hasFDerivAt.cos.differentiableAt
 
 theorem DifferentiableOn.cos (hc : DifferentiableOn ℝ f s) :
     DifferentiableOn ℝ (fun x => Real.cos (f x)) s := fun x h => (hc x h).cos
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.cos (hc : Differentiable ℝ f) : Differentiable ℝ fun x => Real.cos (f x) :=
   fun x => (hc x).cos
 
@@ -839,15 +839,15 @@ theorem DifferentiableWithinAt.sin (hf : DifferentiableWithinAt ℝ f s x) :
     DifferentiableWithinAt ℝ (fun x => Real.sin (f x)) s x :=
   hf.hasFDerivWithinAt.sin.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.sin (hc : DifferentiableAt ℝ f x) :
     DifferentiableAt ℝ (fun x => Real.sin (f x)) x :=
   hc.hasFDerivAt.sin.differentiableAt
 
 theorem DifferentiableOn.sin (hc : DifferentiableOn ℝ f s) :
     DifferentiableOn ℝ (fun x => Real.sin (f x)) s := fun x h => (hc x h).sin
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.sin (hc : Differentiable ℝ f) : Differentiable ℝ fun x => Real.sin (f x) :=
   fun x => (hc x).sin
 
@@ -892,15 +892,15 @@ theorem DifferentiableWithinAt.cosh (hf : DifferentiableWithinAt ℝ f s x) :
     DifferentiableWithinAt ℝ (fun x => Real.cosh (f x)) s x :=
   hf.hasFDerivWithinAt.cosh.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.cosh (hc : DifferentiableAt ℝ f x) :
     DifferentiableAt ℝ (fun x => Real.cosh (f x)) x :=
   hc.hasFDerivAt.cosh.differentiableAt
 
 theorem DifferentiableOn.cosh (hc : DifferentiableOn ℝ f s) :
     DifferentiableOn ℝ (fun x => Real.cosh (f x)) s := fun x h => (hc x h).cosh
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.cosh (hc : Differentiable ℝ f) : Differentiable ℝ fun x => Real.cosh (f x) :=
   fun x => (hc x).cosh
 
@@ -947,15 +947,15 @@ theorem DifferentiableWithinAt.sinh (hf : DifferentiableWithinAt ℝ f s x) :
     DifferentiableWithinAt ℝ (fun x => Real.sinh (f x)) s x :=
   hf.hasFDerivWithinAt.sinh.differentiableWithinAt
 
-@[simp]
+@[simp, fun_prop]
 theorem DifferentiableAt.sinh (hc : DifferentiableAt ℝ f x) :
     DifferentiableAt ℝ (fun x => Real.sinh (f x)) x :=
   hc.hasFDerivAt.sinh.differentiableAt
 
 theorem DifferentiableOn.sinh (hc : DifferentiableOn ℝ f s) :
     DifferentiableOn ℝ (fun x => Real.sinh (f x)) s := fun x h => (hc x h).sinh
 
-@[simp]
+@[simp, fun_prop]
 theorem Differentiable.sinh (hc : Differentiable ℝ f) : Differentiable ℝ fun x => Real.sinh (f x) :=
   fun x => (hc x).sinh
 

MathlibTest/Deriv.lean

@@ -0,0 +1,25 @@
+import Mathlib
+
+/-! Test that `simp` can prove some lemmas about derivatives. -/
+
+open Real
+
+example (x : ℝ) : deriv (fun x => cos x + 2 * sin x) x = -sin x + 2 * cos x := by
+  simp
+
+example (x : ℝ) :
+    deriv (fun x ↦ cos (sin x) * exp x) x = (cos (sin x) - sin (sin x) * cos x) * exp x := by
+  simp; ring
+
+/- for more complicated examples (with more nested functions) you need to increase the
+`maxDischargeDepth`. -/
+
+example (x : ℝ) :
+    deriv (fun x ↦ sin (sin (sin x)) + sin x) x =
+    cos (sin (sin x)) * (cos (sin x) * cos x) + cos x := by
+  simp (maxDischargeDepth := 3)
+
+example (x : ℝ) :
+    deriv (fun x ↦ sin (sin (sin x)) ^ 10 + sin x) x =
+    10 * sin (sin (sin x)) ^ 9 * (cos (sin (sin x)) * (cos (sin x) * cos x)) + cos x := by
+  simp (maxDischargeDepth := 4)