## Stream: new members

### Topic: How to deduce False from -1 = 1 ?

#### Valentin Vinoles (Dec 02 2023 at 21:26):

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 (Dec 02 2023 at 21:32):

simp at h' works

#### Valentin Vinoles (Dec 02 2023 at 21:40):

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

#### Sabrina Jewson (Dec 02 2023 at 21:40):

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

#### David Renshaw (Dec 02 2023 at 21:41):

also hint finds linarith

#### Valentin Vinoles (Dec 03 2023 at 09:38):

@David Renshaw @Sabrina Jewson
Thanks to you two !

Last updated: Dec 20 2023 at 11:08 UTC