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

State before:
ps : List Prop
q : Prop
⊢ ¬andN' ps ¬q → impliesN ps q
Tactic:
induction ps with
| nil => exact notNotElim
| cons p ps ih =>
  simp only [andN', impliesN]
  intro hnpps hp
  have hnpnps := deMorganSmall₃ hnpps
  match hnpnps with
  | .inl hnp => contradiction
  | .inr hnps => exact ih hnps
State after:
no goals

State before:
case nil
q : Prop
⊢ ¬andN' [] ¬q → impliesN [] q
Tactic:
exact notNotElim
State after:
no goals

State before:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬andN' (p :: ps) ¬q → impliesN (p :: ps) q
Tactic:
simp only [andN', impliesN]
State after:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬(p ∧ andN' ps ¬q) → p → impliesN ps q

State before:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
⊢ ¬(p ∧ andN' ps ¬q) → p → impliesN ps q
Tactic:
intro hnpps hp
State after:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
⊢ impliesN ps q

State before:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
⊢ impliesN ps q
Tactic:
have hnpnps := deMorganSmall₃ hnpps
State after:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
hnpnps : ¬p ∨ ¬andN' ps ¬q
⊢ impliesN ps q

State before:
case cons
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
hnpnps : ¬p ∨ ¬andN' ps ¬q
⊢ impliesN ps q
Tactic:
match hnpnps with
| .inl hnp => contradiction
| .inr hnps => exact ih hnps
State after:
no goals

State before:
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
hnpnps : ¬p ∨ ¬andN' ps ¬q
hnp : ¬p
⊢ impliesN ps q
Tactic:
contradiction
State after:
no goals

State before:
q p : Prop
ps : List Prop
ih : ¬andN' ps ¬q → impliesN ps q
hnpps : ¬(p ∧ andN' ps ¬q)
hp : p
hnpnps : ¬p ∨ ¬andN' ps ¬q
hnps : ¬andN' ps ¬q
⊢ impliesN ps q
Tactic:
exact ih hnps
State after:
no goals