Theorem: Smt.Reconstruct.Prop.deMorgan₂ (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:
exact match l with
| [] => by
  simp [orN, notList]
| [t] => by
  simp only [orN, notList]
  simp [andN] at h
  exact notNotIntro h
| h₁::h₂::t => by
  simp only [orN, notList, map]
  simp [andN] at h
  apply deMorganSmall₂
  have nnh₁ := notNotIntro (And.left h)
  have ih := @deMorgan₂ (h₂::t) (And.right h)
  exact ⟨nnh₁, ih⟩
State after:
no goals

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

State before:
l : List Prop
t : Prop
h : andN [t]
⊢ ¬orN (notList [t])
Tactic:
simp only [orN, notList]
State after:
l : List Prop
t : Prop
h : andN [t]
⊢ ¬¬t

State before:
l : List Prop
t : Prop
h : andN [t]
⊢ ¬¬t
Tactic:
simp [andN] at h
State after:
l : List Prop
t : Prop
h : t
⊢ ¬¬t

State before:
l : List Prop
t : Prop
h : t
⊢ ¬¬t
Tactic:
exact notNotIntro h
State after:
no goals

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

State before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : andN (h₁ :: h₂ :: t)
⊢ ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
Tactic:
simp [andN] at h
State after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
⊢ ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))

State before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
⊢ ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
Tactic:
apply deMorganSmall₂
State after:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)

State before:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Tactic:
have nnh₁ := notNotIntro (And.left h)
State after:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)

State before:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Tactic:
have ih := @deMorgan₂ (h₂::t) (And.right h)
State after:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
ih : ¬orN (notList (h₂ :: t))
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)

State before:
case a
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∧ andN (h₂ :: t)
nnh₁ : ¬¬h₁
ih : ¬orN (notList (h₂ :: t))
⊢ ¬¬h₁ ∧ ¬orN ((¬h₂) :: map Not t)
Tactic:
exact ⟨nnh₁, ih⟩
State after:
no goals