-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem mem_of_necessary_assignment {n : Nat} {p : (PosFin n) → Bool} {c : DefaultClause n}
    {l : Literal (PosFin n)} (p_entails_c : p ⊨ c)
    (p'_not_entails_c : (fun v => if v = l.1 then l.2 else p v) ⊭ c) :
    Literal.negate l ∈ Clause.toList c

Proof state:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : ¬p v = true
⊢ l.negate ∈ Clause.toList c

Tactic:
exfalso

Result:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : ¬p v = true
⊢ False

Proof state:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : (if v = l.fst then l.snd else p v) = true
⊢ l.negate ∈ Clause.toList c

Tactic:
split at h

Result:
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negate ∈ Clause.toList c

case intro.inl.intro.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : ¬v = l.fst
h : p v = true
⊢ l.negate ∈ Clause.toList c

Proof state:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : p v = true
⊢ l.negate ∈ Clause.toList c

Tactic:
exfalso

Result:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
hne : ¬v = l.fst
h : p v = true
⊢ False

Proof state:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negate ∈ Clause.toList c

Tactic:
have h := p'_not_entails_c.1 v_in_c

Result:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = false
⊢ l.negate ∈ Clause.toList c

Proof state:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : ¬(if v = l.fst then l.snd else p v) = false
⊢ l.negate ∈ Clause.toList c

Tactic:
simp only [Entails.eval, Bool.not_eq_false] at h

Result:
case intro.inl.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h : (if v = l.fst then l.snd else p v) = true
⊢ l.negate ∈ Clause.toList c

Proof state:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
heq : v = l.fst
h : l.snd = true
⊢ l.negate ∈ Clause.toList c

Tactic:
simp [Literal.negate, ← heq, h, v_in_c]

Result:
no goals

Proof state:
case intro.inl.intro.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, false) ∈ Clause.toList c
pv : p v = false
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
h✝ : v = l.fst
h : l.snd = true
⊢ l.negate ∈ Clause.toList c

Tactic:
next heq => simp [Literal.negate, ← heq, h, v_in_c]

Result:
no goals

Proof state:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ¬∃ a,
      (a, false) ∈ Clause.toList c ∧ (if a = l.fst then l.snd else p a) = false ∨
        (a, true) ∈ Clause.toList c ∧ (if a = l.fst then l.snd else p a) = true
⊢ l.negate ∈ Clause.toList c

Tactic:
simp only [not_exists, not_or, not_and] at p'_not_entails_c

Result:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p_entails_c : ∃ a, (a, false) ∈ Clause.toList c ∧ p a = false ∨ (a, true) ∈ Clause.toList c ∧ p a = true
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
⊢ l.negate ∈ Clause.toList c

Proof state:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
p'_not_entails_c :
  ∀ (x : PosFin n),
    ((x, false) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = false) ∧
      ((x, true) ∈ Clause.toList c → ¬(if x = l.fst then l.snd else p x) = true)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
⊢ l.negate ∈ Clause.toList c

Tactic:
specialize p'_not_entails_c v

Result:
case intro.inr.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
v_in_c : (v, true) ∈ Clause.toList c
pv : p v = true
p'_not_entails_c :
  ((v, false) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = false) ∧
    ((v, true) ∈ Clause.toList c → ¬(if v = l.fst then l.snd else p v) = true)
⊢ l.negate ∈ Clause.toList c