Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not (Lean4Axiomatic/Logic.lean)

State before:
p q : Prop
⊢ ¬(p ∨ q) ↔ ¬p ∧ ¬q
Tactic:
apply Iff.intro
State after:
case mp
p q : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q

case mpr
p q : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)

State before:
p q : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q
Tactic:
case mp =>
  intro (_ : ¬(p ∨ q))
  show ¬p ∧ ¬q
  have : ¬p := by
    intro (_ : p)
    show False
    have : p ∨ q := Or.inl ‹p›
    exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
  have : ¬q := by
    intro (_ : q)
    show False
    have : p ∨ q := Or.inr ‹q›
    exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
  exact And.intro ‹¬p› ‹¬q›
State after:
no goals

State before:
p q : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
case mpr =>
  intro (And.intro (_ : ¬p) (_ : ¬q)) (_ : p ∨ q)
  show False
  match ‹p ∨ q› with
  | Or.inl (_ : p) => exact absurd ‹p› ‹¬p›
  | Or.inr (_ : q) => exact absurd ‹q› ‹¬q›
State after:
no goals

State before:
p q : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q
Tactic:
intro (_ : ¬(p ∨ q))
State after:
p q : Prop
x✝ : ¬(p ∨ q)
⊢ ¬p ∧ ¬q

State before:
p q : Prop
x✝ : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
Tactic:
have : ¬p := by
  intro (_ : p)
  show False
  have : p ∨ q := Or.inl ‹p›
  exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
State after:
p q : Prop
x✝ : ¬(p ∨ q)
this : ¬p
⊢ ¬p ∧ ¬q

State before:
p q : Prop
x✝ : ¬(p ∨ q)
this : ¬p
⊢ ¬p ∧ ¬q
Tactic:
have : ¬q := by
  intro (_ : q)
  show False
  have : p ∨ q := Or.inr ‹q›
  exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
State after:
p q : Prop
x✝ : ¬(p ∨ q)
this✝ : ¬p
this : ¬q
⊢ ¬p ∧ ¬q

State before:
p q : Prop
x✝ : ¬(p ∨ q)
this✝ : ¬p
this : ¬q
⊢ ¬p ∧ ¬q
Tactic:
exact And.intro ‹¬p› ‹¬q›
State after:
no goals

State before:
p q : Prop
x✝ : ¬(p ∨ q)
⊢ ¬p
Tactic:
intro (_ : p)
State after:
p q : Prop
x✝¹ : ¬(p ∨ q)
x✝ : p
⊢ False

State before:
p q : Prop
x✝¹ : ¬(p ∨ q)
x✝ : p
⊢ False
Tactic:
have : p ∨ q := Or.inl ‹p›
State after:
p q : Prop
x✝¹ : ¬(p ∨ q)
x✝ : p
this : p ∨ q
⊢ False

State before:
p q : Prop
x✝¹ : ¬(p ∨ q)
x✝ : p
this : p ∨ q
⊢ False
Tactic:
exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
State after:
no goals

State before:
p q : Prop
x✝ : ¬(p ∨ q)
this : ¬p
⊢ ¬q
Tactic:
intro (_ : q)
State after:
p q : Prop
x✝¹ : ¬(p ∨ q)
this : ¬p
x✝ : q
⊢ False

State before:
p q : Prop
x✝¹ : ¬(p ∨ q)
this : ¬p
x✝ : q
⊢ False
Tactic:
have : p ∨ q := Or.inr ‹q›
State after:
p q : Prop
x✝¹ : ¬(p ∨ q)
this✝ : ¬p
x✝ : q
this : p ∨ q
⊢ False

State before:
p q : Prop
x✝¹ : ¬(p ∨ q)
this✝ : ¬p
x✝ : q
this : p ∨ q
⊢ False
Tactic:
exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
State after:
no goals

State before:
p q : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
intro (And.intro (_ : ¬p) (_ : ¬q)) (_ : p ∨ q)
State after:
p q : Prop
left✝ : ¬p
right✝ : ¬q
x✝ : p ∨ q
⊢ False

State before:
p q : Prop
left✝ : ¬p
right✝ : ¬q
x✝ : p ∨ q
⊢ False
Tactic:
match ‹p ∨ q› with
| Or.inl (_ : p) => exact absurd ‹p› ‹¬p›
| Or.inr (_ : q) => exact absurd ‹q› ‹¬q›
State after:
no goals

State before:
p q : Prop
left✝ : ¬p
right✝ : ¬q
x✝ : p ∨ q
h✝ : p
⊢ False
Tactic:
exact absurd ‹p› ‹¬p›
State after:
no goals

State before:
p q : Prop
left✝ : ¬p
right✝ : ¬q
x✝ : p ∨ q
h✝ : q
⊢ False
Tactic:
exact absurd ‹q› ‹¬q›
State after:
no goals