Functions are unequal if they disagree somewhere

Stream: Is there code for X?

[Eric Wieser]

Do we have something like this anywhere?

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

(context: a lemma added in #11973)

[Floris van Doorn]

It seems like we don't (and we want it of course).

[Eric Wieser]

rw [ne.def, function.funext_iff, not_forall] also closes it, but arguably isn't as nice as having the lemma as it doesn't put ne on the rhs

[Eric Wieser]

Based on the usage in #11973, we might want an alias lemma for the forward direction too, since that's handy for case splits, and matches the usual ext / ext_iff split

[Floris van Doorn]

since a couple days you can spell not_congr h as h.not :-)

[Sebastian Monnet]

@Anne Baanen I'm trying to apply your lemma from the PR, and I'm having some inference issues. Can you see why this doesn't work?

import field_theory.galois

section a
variables (F α : Sort*) (β : α → Sort*)
variables {F α β} [i : fun_like F α β]
include i

lemma fun_like.exists_ne {f g : F} (h : f ≠ g) : ∃ x, f x ≠ g x :=
not_forall.mp $ mt (fun_like.ext _ _) h
end a
example (K L : Type*) [field K] [field L] [algebra K L] (f g : L ≃ₐ[K] L) (h_diff : f ≠ g) :
∃ (x : L), f x ≠ g x :=
begin
  apply fun_like.exists_ne,
end

[Anne Baanen]

It seems like there is a missing fun_like instance:

example (K L : Type*) [field K] [field L] [algebra K L] : fun_like (L ≃ₐ[K] L) L (λ _, L) :=
by apply_instance -- fails

[Yaël Dillies]

Please report stuff like that in https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Morphism.20refactor so that I can keep track of everything that needs changing.

[Anne Baanen]

I'll try and define ring_equiv_class now and instantiate it for alg_equiv too, since I have not much planned this afternoon.

[Yaël Dillies]

Thanks! Then I can finally define order_ring_equiv from #3292

[Anne Baanen]

#11977

[Yaël Dillies]

Reviewed!

[Kyle Miller]

Floris van Doorn said:

since a couple days you can spell not_congr h as h.not :-)

That's great! I've wanted that for a while.

I was wondering a few days ago whether we had gotten around to implementing Eric's suggestion https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Apply.20contrapostive/near/254089346

[Eric Wieser]

I'd forgotten I'd suggested that!

[Eric Wieser]

Do we have docs#iff.and too, or just docs#iff.not?

[Eric Wieser]

Yes! #11803 for the full set