Porting note: `ext` does not look through definitions, so we need more `ext` lemmas

[kim-em]

Classifies porting notes claiming:

added ext lemma
added @[ext]

Links

• Porting note: removed @[ext] #11182: categorises removal of @[ext].
• Porting note: broken ext #11041: categorises other failures of ext.
• Porting note: added theorem / lemma #10756: categorises general addition of theorems

Notes

We could either provide some automation to generate the additional ext lemmas we need now, or work out how to make ext more powerful.

See discussion on zulip: 1.

[kim-em]

This link searches for references to this issue in the source code.