Theorem: Smt.Reconstruct.Prop.deMorgan₃ (Smt/Reconstruct/Prop/Lemmas.lean)

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

State before:
l : List Prop
h : ¬orN l
⊢ andN (notList l)
Tactic:
exact match l with
| [] => True.intro
| [t] => by
  simp only [andN, notList, map]
  simp only [orN, Not] at h
  exact h
| h₁::h₂::t => by
  simp only [orN, Not] at h
  have ⟨t₁, t₂⟩ := deMorganSmall h
  simp only [orN, Not] at t₂
  simp [andN, notList, map]
  have ih := @deMorgan₃ (h₂::t) t₂
  exact ⟨t₁, ih⟩
State after:
no goals

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

State before:
l : List Prop
t : Prop
h : ¬orN [t]
⊢ ¬t
Tactic:
simp only [orN, Not] at h
State after:
l : List Prop
t : Prop
h : t → False
⊢ ¬t

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

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

State before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
⊢ andN (notList (h₁ :: h₂ :: t))
Tactic:
have ⟨t₁, t₂⟩ := deMorganSmall h
State after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : ¬orN (h₂ :: t)
⊢ andN (notList (h₁ :: h₂ :: t))

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

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

State before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : orN (h₂ :: t) → False
⊢ ¬h₁ ∧ andN ((¬h₂) :: map Not t)
Tactic:
have ih := @deMorgan₃ (h₂::t) t₂
State after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : h₁ ∨ orN (h₂ :: t) → False
t₁ : ¬h₁
t₂ : orN (h₂ :: t) → False
ih : andN (notList (h₂ :: t))
⊢ ¬h₁ ∧ andN ((¬h₂) :: map Not t)

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