auto tfae.out lemmas?

Stream: general

[Yury G. Kudryashov]

It would be nice to have a command/attribute/whatever to generate iff lemmas (and possibly dot notation implications) from a tfae lemma. E.g., several lemmas after docs#t1_space_tfae can be autogenerated from the tfae lemma.