## Stream: new members

### Topic: contraposition

#### Henning Dieterichs (Nov 13 2020 at 18:17):

Sorry for this stupid question. My goal is to show A -> B. I would like to rewrite this goal to \neg B -> \neg A. How do I do that? I know I could prove (A -> B) -> (\neg B -> \neg A) and use rewrite, but I was hoping for something built in

#### Kevin Buzzard (Nov 13 2020 at 18:18):

This result will be in the library -- is it called something like neg_imp_neg or something?

#### Henning Dieterichs (Nov 13 2020 at 18:18):

What is the best way to search the library?

#### Kevin Buzzard (Nov 13 2020 at 18:19):

import tactic

example (A B : Prop) : (¬ B → ¬ A) ↔ (A → B) := by library_search


#### Kevin Buzzard (Nov 13 2020 at 18:19):

not_imp_not

#### Kevin Buzzard (Nov 13 2020 at 18:20):

That's one way. Another way is to guess what the result is called using #naming and start to type your guess and see what VS Code predicts. import tactic imports a bunch of stuff, making library_search more likely to succeed.

#### Kevin Buzzard (Nov 13 2020 at 18:21):

As you can see, you tripped me up by calling it neg, but #naming tells us it's called not

#### Henning Dieterichs (Nov 13 2020 at 18:23):

Thanks, I didn't know about these naming guidelines or library_search ;) not_imp_not works as expected

#### Kevin Buzzard (Nov 13 2020 at 18:23):

Yeah, there are a lot of secrets :-) Useful tactics get written much faster than useful documentation of the tactics. https://leanprover-community.github.io/mathlib_docs/tactics.html

#### Henning Dieterichs (Nov 13 2020 at 18:24):

Can I somehow list all tactics that are applicable at the current position?

#### Henning Dieterichs (Nov 13 2020 at 18:25):

Or all lemmas l so that rw l succeeds?

#### Bryan Gin-ge Chen (Nov 13 2020 at 18:25):

tactic#hint for the former, rw_hint is supposed to do the latter, but the PR #2030 was closed without being merged.

#### Bryan Gin-ge Chen (Nov 13 2020 at 18:26):

hint won't give anything like a complete list

#### Bryan Gin-ge Chen (Nov 13 2020 at 18:26):

but maybe it's still useful

#### Henning Dieterichs (Nov 13 2020 at 18:27):

wow, hint is useful, thanks

#### Kevin Buzzard (Nov 13 2020 at 18:27):

PS "stupid" questions are welcome in #new members , you're doing exactly the right thing