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

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

State before:
l : List Prop
h : ¬orN (notList l)
⊢ andN l
Tactic:
exact match l with
| []   => True.intro
| [t]  => by
  simp only [andN]
  simp only [notList, orN, map] at h
  cases Classical.em t with
  | inl tt  => exact tt
  | inr ntt => exact False.elim (h ntt)
| h₁::h₂::t => by
  simp only [orN, notList, map] at h
  have ⟨ t₁, t₂ ⟩ := deMorganSmall h
  have ih := @deMorgan (h₂::t) t₂
  simp [andN]
  have t₁' := notNotElim t₁
  exact ⟨ t₁', ih ⟩
State after:
no goals

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

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

State before:
l : List Prop
t : Prop
h : ¬¬t
⊢ t
Tactic:
cases Classical.em t with
| inl tt  => exact tt
| inr ntt => exact False.elim (h ntt)
State after:
no goals

State before:
case inl
l : List Prop
t : Prop
h : ¬¬t
tt : t
⊢ t
Tactic:
exact tt
State after:
no goals

State before:
case inr
l : List Prop
t : Prop
h : ¬¬t
ntt : ¬t
⊢ t
Tactic:
exact False.elim (h ntt)
State after:
no goals

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

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

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

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

State before:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
ih : andN (h₂ :: t)
⊢ h₁ ∧ andN (h₂ :: t)
Tactic:
have t₁' := notNotElim t₁
State after:
l : List Prop
h₁ h₂ : Prop
t : List Prop
h : ¬(¬h₁ ∨ orN ((¬h₂) :: map Not t))
t₁ : ¬¬h₁
t₂ : ¬orN ((¬h₂) :: map Not t)
ih : andN (h₂ :: t)
t₁' : h₁
⊢ h₁ ∧ andN (h₂ :: t)

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