-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Clause.lean
theorem not_tautology (c : DefaultClause n) (l : Literal (PosFin n)) :
    l ∉ toList c ∨ ¬Literal.negate l ∈ toList c

Proof state:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

Tactic:
rwa [← hl] at h

Result:
no goals

Proof state:
case neg.a
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬(l.fst, true) ∈ c.clause ∨ ¬l ∈ c.clause

Tactic:
rwa [← hl] at h

Result:
no goals

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.toList ∨ ¬l.negate ∈ c.toList

Tactic:
simp only [toList, Literal.negate]

Result:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Proof state:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Tactic:
simp only [Bool.not_eq_true] at hl

Result:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Tactic:
by_cases hl : l.2

Result:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : ¬l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Proof state:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Tactic:
simp only [hl, Bool.not_false]

Result:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

Proof state:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Tactic:
have h := c.nodupkey l.1

Result:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Proof state:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, !l.snd) ∈ c.clause

Tactic:
simp only [hl, Bool.not_true]

Result:
case pos
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = true
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause

Proof state:
case neg
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬l ∈ c.clause ∨ ¬(l.fst, true) ∈ c.clause

Tactic:
apply Or.symm

Result:
case neg.a
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
h : ¬(l.fst, true) ∈ c.clause ∨ ¬(l.fst, false) ∈ c.clause
hl : l.snd = false
⊢ ¬(l.fst, true) ∈ c.clause ∨ ¬l ∈ c.clause