## Stream: general

### Topic: tfae formatting

#### Johan Commelin (Dec 27 2019 at 16:16):

tfae is being used. Kudos to @Reid Barton and @Simon Hudon for making the tactic work, and to @Yury G. Kudryashov for using it.
Here's a question/proposal about formatting: shall we format tfae statements with one "item" per line?
Pinging @Mario Carneiro and @Rob Lewis for this style issue.

#### Yury G. Kudryashov (Dec 27 2019 at 16:18):

Do you mean something like this?

lemma tfae_mem_nhds_within_Ioi {a u' : α} (hu' : a < u') (s : set α) :
tfae [s ∈ nhds_within a (Ioi a), /- 0 -/
s ∈ nhds_within a (Ioc a u'), /- 1 -/
s ∈ nhds_within a (Ioo a u'), /- 2 -/
∃ u ∈ Ioc a u', Ioo a u ⊆ s, /- 3 -/
∃ u ∈ Ioi a, Ioo a u ⊆ s] /- 4 -/ :=


Yes, exactly

#### Yury G. Kudryashov (Dec 27 2019 at 16:19):

Numbers help those writing (tfae_mem_nhds_within_Ioi h s).out 0 3

#### Johan Commelin (Dec 27 2019 at 16:20):

Hmmm, I now realise that tfae_have uses 1-based indexing, but tfae.out uses 0-based indexing...

#### Johan Commelin (Dec 27 2019 at 16:20):

I guess that should be fixed

#### Yury G. Kudryashov (Dec 27 2019 at 16:21):

Or even

lemma tfae_mem_nhds_within_Ioi {a b : α} (h : a < b) (s : set α) :
tfae [s ∈ nhds_within a (Ioi a), /- 0 : s is a neighborhood of a within (a, +∞) -/
s ∈ nhds_within a (Ioc a b), /- 1 : s is a neighborhood of a within (a, b] -/
s ∈ nhds_within a (Ioo a b), /- 2 : s is a neighborhood of a within (a, b) -/
∃ u ∈ Ioc a b, Ioo a u ⊆ s, /- 3 : s includes (a, u) for some u ∈ (a, b] -/
∃ u ∈ Ioi a, Ioo a u ⊆ s] /- 4 : s includes (a, u) for some u > a -/ :=


#### Johan Commelin (Dec 27 2019 at 16:21):

I think I would put := before comment 4

#### Johan Commelin (Dec 27 2019 at 16:21):

But that's minor nitpicking

#### Sebastien Gouezel (Dec 27 2019 at 16:22):

Also, for one-line comments you can use --.

#### Johan Commelin (Dec 27 2019 at 16:22):

Only if you don't put := at the end of the line

#### Sebastien Gouezel (Dec 27 2019 at 16:23):

Yes. I was implicitly seconding your comment :)

#### Yury G. Kudryashov (Dec 27 2019 at 16:23):

lemma tfae_mem_nhds_within_Ioi {a b : α} (h : a < b) (s : set α) :
tfae [s ∈ nhds_within a (Ioi a), -- 0 : s is a neighborhood of a within (a, +∞)
s ∈ nhds_within a (Ioc a b),   -- 1 : s is a neighborhood of a within (a, b]
s ∈ nhds_within a (Ioo a b),   -- 2 : s is a neighborhood of a within (a, b)
∃ u ∈ Ioc a b, Ioo a u ⊆ s,    -- 3 : s includes (a, u) for some u ∈ (a, b]
∃ u ∈ Ioi a, Ioo a u ⊆ s] :=   -- 4 : s includes (a, u) for some u > a


#### Johan Commelin (Dec 27 2019 at 16:24):

It's too bad that those comments won't end up in the docstring

#### Johan Commelin (Dec 27 2019 at 16:34):

In fact, I think it's quite important that these comments do end up in the docstring, because if the lemma gets used with tfae.out a person reading the code will probably want to hover over the lemma to see exactly which two equivalent statements are being used.

#### Yury G. Kudryashov (Dec 27 2019 at 16:40):

I'll copy them to the docstring.

#### Rob Lewis (Dec 27 2019 at 19:45):

I agree that the 0/1 indexing should be made consistent and that the numbers should appear in the docstring.

#### Rob Lewis (Dec 27 2019 at 19:46):

Note that (I think) markdown will format a numbered list starting with 1, even if the input starts with 0. i.e.

0. s is a neighborhood...
1. s is a neighborhood...


will get printed as

1. ...
2. ...


#### Rob Lewis (Dec 27 2019 at 19:47):

So maybe we should use 1-based indexing. Or unordered lists with indices added manually.

#### Mario Carneiro (Dec 27 2019 at 23:45):

Actually, I think we could use an annotation so that we can write:

lemma tfae_mem_nhds_within_Ioi {a b : α} (h : a < b) (s : set α) :
by tfae [
Ioi: s ∈ nhds_within a (Ioi a),
Ioc: s ∈ nhds_within a (Ioc a b),
Ioo: s ∈ nhds_within a (Ioo a b),
ex_Ioc: ∃ u ∈ Ioc a b, Ioo a u ⊆ s,
ex_Ioi: ∃ u ∈ Ioi a, Ioo a u ⊆ s] :=


and then reference the names using tfae_have Ioi <-> Ioo := tfae_mem_nhds_within_Ioi or similar

#### Mario Carneiro (Dec 27 2019 at 23:47):

It could be syntax for tfae [(\lam Ioi, Ioi) s ∈ nhds_within a (Ioi a), ...

#### Johan Commelin (Dec 28 2019 at 07:40):

I think I could have made tfae_have use 0-based indexing. But these new suggestions go beyond my skill set. They do look fancy. @Mario Carneiro Would tfae.out be able to use those indices as well?

#### Mario Carneiro (Dec 28 2019 at 08:07):

if by tfae.out you mean the term, no

#### Mario Carneiro (Dec 28 2019 at 08:07):

I would also suggest keeping zero based indexing in tfae.out