Inequality from inequality

Stream: new members

[Hungry Applicative]

Is there an existing theorem expressing the inference a ≠ b from f a ≠ f b?

I have a proof here using classical reasoning:

theorem congrArgDual {α β: Type} {a₁ a₂: α} (f: α → β) (h₀: f a₁ ≠ f a₂ ) : a₁ ≠ a₂ :=
  byContradiction
    fun h₁: ¬¬(a₁ = a₂) =>
    have h₂: a₁ = a₂ := dn h₁
    have h₄: f a₁ = f a₂ := congrArg f h₂
    show False from h₀ h₄

[Ruben Van de Velde]

I don't think you need classical reasoning - maybe:

theorem congrArgDual {α β: Type} {a₁ a₂: α} (f: α → β) (h₀: f a₁ ≠ f a₂ ) : a₁ ≠ a₂ :=
    fun h₁: (a₁ = a₂) =>
    have h₄: f a₁ = f a₂ := congrArg f h₁
    show False from h₀ h₄

[Hungry Applicative]

That's much better. Thanks! I am completely new to atp. Have you come across a similar theorem before? It seems generally useful.

[Kyle Miller]

In mathlib it's called docs#ne_of_apply_ne

[Eric Wieser]

And the reverse direction is docs#function.injective.ne