ext/funext

Stream: mathlib4

[Adam Topaz]

Does Mathlib4's ext tactic not apply funext? I ran into this issue a couple of times in !4#2424 and it seems that !4#2418 is also affected.
Is this expected behavior?

[Gabriel Ebner]

Probably because ⟶ is no longer reducibly a function. The old ext had a fall back where it tried to apply all ext-lemmas before failing, and that's likely why it succeeded here.

[Gabriel Ebner]

The intended solution here is to add an extensionality lemma for the type Prefunctor.obj (Prefunctor.obj coyoneda.toPrefunctor (Opposite.op (Prefunctor.obj F'.toPrefunctor x))).toPrefunctor f ⟶ Prefunctor.obj (Prefunctor.obj coyoneda.toPrefunctor (Opposite.op (Prefunctor.obj F.toPrefunctor x))).toPrefunctor f (at a reasonable generality of course).