How to deduce False from -1 = 1 ?

Stream: new members

[Valentin Vinoles]

Hello ,

I am trying to prove that the square function is not injective over the integers. So far I done the following:

import Mathlib

open Function

def f (n : ℤ) := n^2

example : ¬(Injective f) := by
  intro h                         -- h: Injective f
                                  -- ⊢ False
  have h' : f (1) = f (-1) := by  -- h': f (1) = f (-1)
    unfold f
    norm_num
  apply h at h'                   -- h': 1 = -1

But I am stuck here, I am not sure how to deduce False from h'. I tried apply? and exact? but it did not help. Searching in the Mathlib doc did not help either.

[David Renshaw]

simp at h' works

[Valentin Vinoles]

Ho it was easy, I feel dumb right now. Thanks a lot!

[Sabrina Jewson]

norm_num at h'/revert h'; norm_num also, and they work more generally for cases like -1 = 2

[David Renshaw]

also hint finds linarith

[Valentin Vinoles]

@David Renshaw @Sabrina Jewson
Thanks to you two !