tactic wishlist?

Stream: new members

[Patrick Thomas]

I am starting to look at tactic writing and I am looking for ideas for tactics to write that might be useful. Is there a wishlist or something similar somewhere?

[Yury G. Kudryashov]

It would be nice to have a way to tag the lemma docs#real.has_deriv_at_cos with some attribute and have Lean define the next few lemmas in the file (has_deriv_within_at, continuous_at, diferentiable_at, differentiable, continuous, deriv, deriv_within). Or have a command that generates standard lemmas about equivs like docs#equiv.surjective or docs#equiv.apply_eq_iff_eq_symm_apply for a new equivalence (e.g., docs#linear_equiv) using proofs like linear_equiv.to_equiv.apply_symm_apply.

[Yury G. Kudryashov]

(this is (a part of) my personal wish list)

[Bryan Gin-ge Chen]

There are a bunch of requests in mathlib's issues.

[Bryan Gin-ge Chen]

Oh, there's a thread in the general stream too.

[Patrick Thomas]

Bryan Gin-ge Chen said:

Oh, there's a thread in the general stream too.

Oops.

[Patrick Thomas]

Thank you.