## Stream: maths

### Topic: absurd

#### orlando (Apr 22 2020 at 19:29):

Hello
I don't very use often proof by contradiction, and it's my first in lean

i don't understand how to start i proof by contradiction, introducing x0  s.t  not P x to use hyp on x0 ?

example (X :Type) (P : X → Prop ) (hyp : (∃ x : X, ¬ (P x)) → false ) : ∀ x, P x := begin
sorry,
end


#### Alex J. Best (Apr 22 2020 at 19:39):

Using @Patrick Massot 's contrapose tactic

import tactic.push_neg
example (X :Type) (P : X → Prop ) (hyp : (∃ x : X, ¬ (P x)) → false ) : ∀ x, P x := begin
contrapose! hyp,
use hyp,
end


#### Bryan Gin-ge Chen (Apr 22 2020 at 19:40):

This particular result is already in the library as one direction of not_exists_not. Here are a few other ways to prove it:

import tactic

open_locale classical

#check @not_exists_not

example (X :Type) (P : X → Prop ) (hyp : (∃ x : X, ¬ (P x)) → false ) : ∀ x, P x := begin
by_contra H,
rw not_forall at H,
exact hyp H,
end

example (X :Type) (P : X → Prop ) (hyp : (∃ x : X, ¬ (P x)) → false ) : ∀ x, P x := begin
change ¬ _ at hyp,
push_neg at hyp,
assumption,
end


#### orlando (Apr 22 2020 at 19:43):

ohh thx @Patrick Massot and @Alex J. Best :big_smile:

#### orlando (Apr 22 2020 at 19:44):

and @Bryan Gin-ge Chen

Last updated: May 11 2021 at 16:22 UTC