Theorem: not_or_iff_and_not (meetings/Foundations.lean)

State before:
p q r : Prop
⊢ ¬(p ∨ q) ↔ ¬p ∧ ¬q
Tactic:
constructor
State after:
case mp
p q r : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q

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

State before:
case mp
p q r : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q

case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
{ intro hnor
  constructor
  { intro hp
    exact hnor (Or.inl hp)
  }
  { intro hq
    exact hnor (Or.inr hq)
  }
}
State after:
case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)

State before:
case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
{ 
  intros hnand hor
  rcases hnand with ⟨hnp, hnq⟩  
  cases hor with
    | inl hp => exact hnp hp
    | inr hq => exact hnq hq
}
State after:
no goals

State before:
case mp
p q r : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q
Tactic:
intro hnor
State after:
case mp
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p ∧ ¬q

State before:
case mp
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
Tactic:
constructor
State after:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p

case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q

State before:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p

case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q
Tactic:
{ intro hp
  exact hnor (Or.inl hp)
}
State after:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q

State before:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q
Tactic:
{ intro hq
  exact hnor (Or.inr hq)
}
State after:
no goals

State before:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬p
Tactic:
intro hp
State after:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
hp : p
⊢ False

State before:
case mp.left
p q r : Prop
hnor : ¬(p ∨ q)
hp : p
⊢ False
Tactic:
exact hnor (Or.inl hp)
State after:
no goals

State before:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
⊢ ¬q
Tactic:
intro hq
State after:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
hq : q
⊢ False

State before:
case mp.right
p q r : Prop
hnor : ¬(p ∨ q)
hq : q
⊢ False
Tactic:
exact hnor (Or.inr hq)
State after:
no goals

State before:
case mpr
p q r : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
intros hnand hor
State after:
case mpr
p q r : Prop
hnand : ¬p ∧ ¬q
hor : p ∨ q
⊢ False

State before:
case mpr
p q r : Prop
hnand : ¬p ∧ ¬q
hor : p ∨ q
⊢ False
Tactic:
rcases hnand with ⟨hnp, hnq⟩
State after:
case mpr.intro
p q r : Prop
hor : p ∨ q
hnp : ¬p
hnq : ¬q
⊢ False

State before:
case mpr.intro
p q r : Prop
hor : p ∨ q
hnp : ¬p
hnq : ¬q
⊢ False
Tactic:
cases hor with
  | inl hp => exact hnp hp
  | inr hq => exact hnq hq
State after:
no goals

State before:
case mpr.intro.inl
p q r : Prop
hnp : ¬p
hnq : ¬q
hp : p
⊢ False
Tactic:
exact hnp hp
State after:
no goals

State before:
case mpr.intro.inr
p q r : Prop
hnp : ¬p
hnq : ¬q
hq : q
⊢ False
Tactic:
exact hnq hq
State after:
no goals