iff lemmas for equivs

Stream: mathlib4

[Yury G. Kudryashov]

We have many lemmas like docs#Homeomorph.isCompact_image. How hard is it to autogenerate them?

• Ideally, they should be completely autogenerated: the definition of IsCompact only uses topology and homeomorphisms preserve topology. AFAIR, I was told that it's hard. Also, we usually want to prove one of implications with much weaker assumptions on the map.
• Less automatic approach is to autogenerate both docs#Homeomorph.isCompact_image and docs#Homeomorph.isCompact_preimage from one implication, giving user a choice between preimage (easy for IsOpen) and image (easy for IsCompact).
• Or tell me that the time of people who can write meta code is too valuable to automate such small particular cases (properties of sets under EquivLike maps).

[Scott Morrison]

Jake Levinson and I have been thinking again about auto-generation, but no promises. :-)

[Johan Commelin]

The 2nd half of your first bullet point is why I think this automation never became very urgent in practice.

[Scott Morrison]

Our auto-generation method is meant to work in just one direction at a time, and to just pick up surjective / injective / etc hypotheses as needed.