Disha Sharma

Stream: new members

[Disha Sharma]

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

[Disha Sharma]

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

[Disha Sharma]

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

[Notification Bot]

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

[Notification Bot]

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

[Notification Bot]

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

[Eric Wieser]

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

[Scott Morrison]

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

[Disha Sharma]

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]

Can you edit your message to use #backticks?

[Scott Morrison]

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

[Scott Morrison]

import Mathlib

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

[Scott Morrison]

(exact? will also find the other direction)