## Stream: new members

### Topic: Why are two simps needed here?

#### Terence Tao (Oct 20 2023 at 16:10):

Why is one simp insufficient to prove this statement:

import Mathlib
import Mathlib.Tactic
import Mathlib.Analysis.SpecialFunctions.Pow.Real

example (a: ) : Differentiable  (fun (x:)  (Real.exp x + a)) := by
simp
apply Differentiable.exp
simp

Differentiable.exp is a simp lemma, so I would have thought simp would automatically invoke it.

#### Alex J. Best (Oct 20 2023 at 16:35):

docs#Differentiable.exp says that Differentiable ℝ fun x => Real.exp (f x) for all differentiable f, whereas your goal is Differentiable ℝ fun y => Real.exp y which doesnt have an f in so they are syntactically different. simp only does matching up to syntax, so it won't insert identity functions for instance, which is what we would want to happen implicitly here.
In this situation we normally make two lemmas for the library, like docs#Real.continuous_exp and docs#Continuous.exp one of which is compositional, and one which is just the statement about the literal exp function.

#### Alex J. Best (Oct 20 2023 at 16:40):

One thing you could do in this particular example is write

simpa using Differentiable.exp (f := id)

but its hard to know that this would be needed without first writing the proof you wrote. Ideally we will at some point have a differentiability tactic that automates these proofs in the same way that we have continuity, but we don't have it yet.

#### Mauricio Collares (Oct 20 2023 at 16:42):

I don't necessarily recommend term mode proofs here, but to exemplify what Alex said about composability,

example (a: ) : Differentiable  (fun (x:)  (Real.exp x + a)) := Real.differentiable_exp.add_const a

and

example (a: ) : Differentiable  (fun (x:)  (Real.exp x + a)) := differentiable_id.exp.add_const a

both work (and the autocomplete is pretty good).

#### Jireh Loreaux (Oct 20 2023 at 17:17):

I believe the way to create the automation Alex is describing is to use aesop (Automated Extensible Search for Obvious Proofs), like so:

import Mathlib

open Real

attribute [aesop safe apply]
Differentiable.exp
Real.differentiable_exp
differentiable_id
differentiable_const

example (a : ) : Differentiable  (fun x :   exp x + a) := by aesop

aesop is new to Lean 4, and mathlib is not yet making use of it to its fullest extent. We are still learning some lessons about how to tag lemmas with aesop appropriately. I'm just adding this here to showcase that this kind of automation is possible, and lies in the relatively near future.

#### Adomas Baliuka (Oct 21 2023 at 22:39):

Should I request permission and PR the differentiability tactic which one gets from shamelessly copying continuity (it does basically what Jireh just showed)? I tried this out recently but the discussion about it died. There seemed to be some suboptimal things going on with continuity as well, so maybe one should wait. On the other hand, I'm not sure anyone is working on it (or if people are actually using continuity that much)...

#### Alex J. Best (Oct 21 2023 at 22:46):

YesI think you should definitely PR a differentiability tactic, that would be great!
I think these tactics are certainly useful enough to be worth writing (especially if the implementation with aesop is short)