negation of funext?

Stream: Is there code for X?

[Eric Rodriguez]

Does example (f : α → β) (g : α → β) : f ≠ g ↔ ∃ a : α, f a ≠ g a exist? I've looked everywhere and I can't find it at all, but I refuse to believe this isn't in mathlib

[Ruben Van de Velde]

Apparently not? If you need a proof:

example {α β : Type*} (f : α → β) (g : α → β) : f ≠ g ↔ ∃ a : α, f a ≠ g a :=
(not_congr function.funext_iff).trans not_forall

[Eric Rodriguez]

Proof was no big dealio was just confused it wasn't in mathlib ;b Feels like something worth PRing, I'd do it but you've written all the code now! Not sure where it'd fit in, maybe in logic.function.basic?

[Eric Wieser]

This doesn't scale very well - if we're going to add this lemma, we will probably want to add such a variant for every ext lemma in mathlib.

[Kevin Buzzard]

I guess if we have 1000 proofs of $A\iff B$ then I'm not sure we want 1000 new proofs of $\lnot A\iff \lnot B$.

[Eric Rodriguez]

Would it maybe work better as an extension to the ext tactic, maybe ext!?

[Eric Wieser]

What's the goal state you ended up needing this for, @Eric Rodriguez?

[Eric Rodriguez]

Just looked, and I ended up deleting it, and just usingcontrapose! earlier. It probably makes the code far more readable, tbh