Theorem: not_and_iff_or_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 hnand
  by_cases p 
  { exact Or.inr λ hq => hnand ⟨h, hq⟩}
  { left
    exact h
  }
}
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 hnor hand
  rcases hand with ⟨hp, hq⟩  
  cases hnor with
    | inl hnp => exact hnp hp
    | inr hnq => exact hnq hq
}
State after:
no goals

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

State before:
case mp
p q r : Prop
hnand : ¬(p ∧ q)
⊢ ¬p ∨ ¬q
Tactic:
by_cases p
State after:
case pos
p q r : Prop
hnand : ¬(p ∧ q)
h : p
⊢ ¬p ∨ ¬q

case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q

State before:
case pos
p q r : Prop
hnand : ¬(p ∧ q)
h : p
⊢ ¬p ∨ ¬q

case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
Tactic:
{ exact Or.inr λ hq => hnand ⟨h, hq⟩}
State after:
case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q

State before:
case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
Tactic:
{ left
  exact h
}
State after:
no goals

State before:
case pos
p q r : Prop
hnand : ¬(p ∧ q)
h : p
⊢ ¬p ∨ ¬q
Tactic:
exact Or.inr λ hq => hnand ⟨h, hq⟩
State after:
no goals

State before:
case neg
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p ∨ ¬q
Tactic:
left
State after:
case neg.h
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p

State before:
case neg.h
p q r : Prop
hnand : ¬(p ∧ q)
h : ¬p
⊢ ¬p
Tactic:
exact h
State after:
no goals

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

State before:
case mpr
p q r : Prop
hnor : ¬p ∨ ¬q
hand : p ∧ q
⊢ False
Tactic:
rcases hand with ⟨hp, hq⟩
State after:
case mpr.intro
p q r : Prop
hnor : ¬p ∨ ¬q
hp : p
hq : q
⊢ False

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

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

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