What is the correct/preferred way to TFAE

Stream: new members

[kvanvels]

I am trying to express a theorem that is structure like : The following are three propositions are equivalent:
1) proposition A
2) proposition B
3) proposition C

My proof will most likely be A \to B, B \to C, and C \to A.
What is a the preferred/correct way to write this up? Is there any example in mathlib or elsewhere that uses this kind of proof/theorem?

I appreciate any direction. I am using lean4 but lean3 ideas will be very much appreciated.

[Junyan Xu]

docs#list.tfae

[Adam Topaz]

And to use it we have docs#list.tfae.out

[kvanvels]

Thanks, this community is great. Thank you. I will follow up if I have more questions.

[Adam Topaz]

I would also look at the tactic list and search for tfae

[Adam Topaz]

We have some nice helper tactics for proving such statements

[Junyan Xu]

Notice that docs#tactic.interactive.tfae_have use 1-based indexing but docs#list.tfae.out is 0-based, if I recall correctly.

[Adam Topaz]

yeah, this inconsistency is annoying

[Eric Wieser]

Note that often what actually happens is that we choose A as the canonical definition and call it my_prop, then write the lemmas my_prop <-> A (by definition), my_prop <-> B, my_prop <-> C

[Eric Wieser]

In my experience, tfae is nice for transcribing a pen and paper result, but not all that convenient for building things on top of.

[Adam Topaz]

It's nice when you have more than 3 statements

[Eric Wieser]

I guess for the case I describe you might use tfae under the hood to build the API

[Adam Topaz]

Or some giant connected digraph of implications and you don't want to manually construct a path between two nodes