## Stream: Is there code for X?

### Topic: negation of funext?

#### Eric Rodriguez (Apr 07 2021 at 11:09):

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 (Apr 07 2021 at 11:38):

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 (Apr 07 2021 at 11:41):

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 (Apr 07 2021 at 11:49):

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 (Apr 07 2021 at 11:57):

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 (Apr 07 2021 at 11:57):

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

#### Eric Wieser (Apr 07 2021 at 14:01):

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

#### Eric Rodriguez (Apr 07 2021 at 14:03):

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

Last updated: May 19 2021 at 02:10 UTC