Theorem: LRAT.Literal.sat_negate_iff_not_sat (LeanSAT/LRAT/CNF.lean)

State before:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p ⊨ l.negateLiteral ↔ ¬(p ⊨ l)
Tactic:
simp only [negateLiteral, sat_iff]
State after:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd ↔ ¬(p ⊨ l)

State before:
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd ↔ ¬(p ⊨ l)
Tactic:
constructor
State after:
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)

case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd

State before:
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)

case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd
Tactic:
. intro h pl
  rw [sat_iff, h, not] at pl
  split at pl <;> simp_all
State after:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd

State before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd
Tactic:
. intro h
  rw [sat_iff] at h
  rw [not]
  split <;> simp_all
State after:
no goals

State before:
case mp
α : Type u_1
p : α → Bool
l : Literal α
⊢ p l.fst = !l.snd → ¬(p ⊨ l)
Tactic:
intro h pl
State after:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : p ⊨ l
⊢ False

State before:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl : p ⊨ l
⊢ False
Tactic:
rw [sat_iff, h, not] at pl
State after:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl :
  (match l.snd with
    | true => false
    | false => true) =
    l.snd
⊢ False

State before:
case mp
α : Type u_1
p : α → Bool
l : Literal α
h : p l.fst = !l.snd
pl :
  (match l.snd with
    | true => false
    | false => true) =
    l.snd
⊢ False
Tactic:
split at pl <;> simp_all
State after:
no goals

State before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
⊢ ¬(p ⊨ l) → p l.fst = !l.snd
Tactic:
intro h
State after:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬(p ⊨ l)
⊢ p l.fst = !l.snd

State before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬(p ⊨ l)
⊢ p l.fst = !l.snd
Tactic:
rw [sat_iff] at h
State after:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst = !l.snd

State before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst = !l.snd
Tactic:
rw [not]
State after:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst =
    match l.snd with
    | true => false
    | false => true

State before:
case mpr
α : Type u_1
p : α → Bool
l : Literal α
h : ¬p l.fst = l.snd
⊢ p l.fst =
    match l.snd with
    | true => false
    | false => true
Tactic:
split <;> simp_all
State after:
no goals