Theorem: Smt.Reconstruct.Prop.notAnd (Smt/Reconstruct/Prop/Lemmas.lean)

State before:
⊢ ∀ (l : List Prop), ¬andN l → orN (notList l)
Tactic:
intros l h
State after:
l : List Prop
h : ¬andN l
⊢ orN (notList l)

State before:
l : List Prop
h : ¬andN l
⊢ orN (notList l)
Tactic:
match l with
| []         => exact False.elim (h True.intro)
| [_]        => exact h
| p₁::p₂::ps => simp [orN, notList, map]
                match deMorganSmall₃ h with
                | Or.inl hnp₁ => exact Or.inl hnp₁
                | Or.inr hnAndTail =>
                  have IH := notAnd (p₂::ps) hnAndTail
                  exact Or.inr IH
State after:
no goals

State before:
l : List Prop
h : ¬andN []
⊢ orN (notList [])
Tactic:
exact False.elim (h True.intro)
State after:
no goals

State before:
l : List Prop
head✝ : Prop
h : ¬andN [head✝]
⊢ orN (notList [head✝])
Tactic:
exact h
State after:
no goals

State before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ orN (notList (p₁ :: p₂ :: ps))
Tactic:
simp [orN, notList, map]
State after:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)

State before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Tactic:
match deMorganSmall₃ h with
| Or.inl hnp₁ => exact Or.inl hnp₁
| Or.inr hnAndTail =>
  have IH := notAnd (p₂::ps) hnAndTail
  exact Or.inr IH
State after:
no goals

State before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
hnp₁ : ¬p₁
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Tactic:
exact Or.inl hnp₁
State after:
no goals

State before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
hnAndTail : ¬andN (p₂ :: ps)
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Tactic:
have IH := notAnd (p₂::ps) hnAndTail
State after:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
hnAndTail : ¬andN (p₂ :: ps)
IH : orN (notList (p₂ :: ps))
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)

State before:
l : List Prop
p₁ p₂ : Prop
ps : List Prop
h : ¬andN (p₁ :: p₂ :: ps)
hnAndTail : ¬andN (p₂ :: ps)
IH : orN (notList (p₂ :: ps))
⊢ ¬p₁ ∨ orN ((¬p₂) :: map Not ps)
Tactic:
exact Or.inr IH
State after:
no goals