## Stream: new members

### Topic: Disha Sharma

#### Disha Sharma (Aug 02 2023 at 11:17):

How can I prove this in Lean (using open classical)
(h: (¬ A ∨ ¬ B)): ¬ (A ∧ B)

#### Disha Sharma (Aug 02 2023 at 11:17):

How can I prove this in Lean (using open classical)
(h: (¬ A ∨ ¬ B)): ¬ (A ∧ B)

#### Disha Sharma (Aug 02 2023 at 11:18):

How can I prove this in Lean (using open classical)
(h: (¬ A ∨ ¬ B)): ¬ (A ∧ B)

#### Notification Bot (Aug 02 2023 at 11:21):

A message was moved here from #new members > Why is [field F] not an implicit argument? by Eric Wieser.

#### Notification Bot (Aug 02 2023 at 11:22):

A message was moved here from #lean4 > Recursive proposition definition by Eric Wieser.

#### Notification Bot (Aug 02 2023 at 11:23):

A message was moved here from #general > Getting Started With Lean Theorem Provers by Eric Wieser.

#### Eric Wieser (Aug 02 2023 at 11:23):

Please don't post a message multiple times in different topics, especially if your message is not related to those topics!

#### Scott Morrison (Aug 02 2023 at 11:55):

@Disha Sharma, what have you tried so far? Can you post a #mwe?

#### Disha Sharma (Aug 02 2023 at 12:07):

I am able to prove the inverse but cannot prove the original statement.
example (h : ¬ (A ∧ B)) : (¬ A ∨ ¬ B) :=
or.elim (em A)
(assume a : A,
have ¬ B, from
(assume b : B,
have and : A ∧ B, from and.intro a b,
show false, from h and),
show (¬ A ∨ ¬ B), from or.inr this)

#### Eric Wieser (Aug 02 2023 at 12:24):

Can you edit your message to use #backticks?

#### Scott Morrison (Aug 02 2023 at 12:29):

Also, you should consider moving to Lean 4. Lean 3 is end-of-life now!

#### Scott Morrison (Aug 02 2023 at 12:30):

import Mathlib

example (h : ¬ (A ∧ B)) : (¬ A ∨ ¬ B) := by
exact?   -- Try this: exact Iff.mp not_and_or h


#### Scott Morrison (Aug 02 2023 at 12:31):

(exact? will also find the other direction)

Last updated: Dec 20 2023 at 11:08 UTC