differentiability tactic

Stream: general

[James Arthur]

I created an adapted version of the continuity tactic for differentiable_at type goals, which is here: https://gist.github.com/jamesa9283/400a021c9fc6d3c862914ca7c1d0dace
and @Shing Tak Lam and I were talking about implementing similar things for measurability and integrability and talk of a more general analysis tactic to do all of these arose, is this a good idea? I feel it would be useful as I find the differentiability and continuity useful on their own so one that does all would be amazing in my opinion and I don't want to create three copies of basically the same thing.

simp {discharger := differentiability} also solves deriv goals, as probably expected.

[Hanting Zhang]

I think this is a good idea. In fact I wanted to do it but got scared at the prospect of writing tactics. :upside_down: I've run into places where I want to prove something is integrable and end up writing apply continuous.integrable, continuity or apply integrable.integrable_on, apply continuous.integrable, continuity, etc, a bunch of times.

[Benjamin Davidson]

I was thinking about this the other day. I don't know anything about tactics other than how to use them but I think some sort of integrability tactic would be great!

[Bryan Gin-ge Chen]

@James Arthur If you find the tactic useful, go ahead and make a PR! (You should add some tests in your PR as well, cf. the continuity tests.)

[James Arthur]

So I should PR differentiability on its own? Or develop a more general analysis tactic and then PR?

[Scott Morrison]

The tactic itself doesn't seem to have anything to do with analysis!

[Scott Morrison]

It would definitely be good to have a generalization.