-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RatAddSound.lean
theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c : DefaultClause n}
    {l : Literal (PosFin n)} (p_entails_cl : p ⊨ c.delete (Literal.negate l)) :
    (fun v => if v = l.1 then l.2 else p v) ⊨ c.delete (Literal.negate l)

Proof state:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negate) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negate) ∧ (if a = l.fst then l.snd else p a) = true

Tactic:
exists v

Result:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negate) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negate) ∧ (if v = l.fst then l.snd else p v) = true

Proof state:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
hne : ¬v = l.fst
⊢ p v = false

Tactic:
exact pv

Result:
no goals

Proof state:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negate) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negate) ∧ (if a = l.fst then l.snd else p a) = true

Tactic:
exists v

Result:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negate) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negate) ∧ (if v = l.fst then l.snd else p v) = true

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

Tactic:
rcases p_entails_cl with ⟨v, ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩ | ⟨⟨negl_ne_v, v_in_c_del_l⟩, pv⟩⟩

Result:
case intro.inl.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negate) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negate) ∧ (if a = l.fst then l.snd else p a) = true

case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ ∃ a,
    (a, false) ∈ Clause.toList (c.delete l.negate) ∧ (if a = l.fst then l.snd else p a) = false ∨
      (a, true) ∈ Clause.toList (c.delete l.negate) ∧ (if a = l.fst then l.snd else p a) = true

Proof state:
case intro.inl.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negate)

Tactic:
simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]

Result:
no goals

Proof state:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
v_in_c_del_l : (v, false) ∈ c.toList
heq : v = l.fst
negl_ne_v : ¬false = !l.snd
⊢ l.snd = false

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.inl.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = false

Tactic:
split

Result:
case intro.inl.intro.intro.h.right.isTrue
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
h✝ : v = l.fst
⊢ l.snd = false

case intro.inl.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = false

Proof state:
case intro.inr.intro.intro
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, false) ∈ Clause.toList (c.delete l.negate) ∧ (if v = l.fst then l.snd else p v) = false ∨
    (v, true) ∈ Clause.toList (c.delete l.negate) ∧ (if v = l.fst then l.snd else p v) = true

Tactic:
right

Result:
case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negate) ∧ (if v = l.fst then l.snd else p v) = true

Proof state:
case intro.inl.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = false
negl_ne_v : (v, false) ≠ l.negate
v_in_c_del_l : (v, false) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = false

Tactic:
next hne =>
exact pv

Result:
no goals

Proof state:
case intro.inr.intro.intro.h
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negate) ∧ (if v = l.fst then l.snd else p v) = true

Tactic:
constructor

Result:
case intro.inr.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negate)

case intro.inr.intro.intro.h.right
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (if v = l.fst then l.snd else p v) = true

Proof state:
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
hne : ¬v = l.fst
⊢ p v = true

Tactic:
exact pv

Result:
no goals

Proof state:
case intro.inr.intro.intro.h.left
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
⊢ (v, true) ∈ Clause.toList (c.delete l.negate)

Tactic:
simp [Clause.toList, delete_iff, negl_ne_v, v_in_c_del_l]

Result:
no goals

Proof state:
case intro.inr.intro.intro.h.right.isFalse
n : Nat
p : PosFin n → Bool
c : DefaultClause n
l : Literal (PosFin n)
v : PosFin n
pv : p v = true
negl_ne_v : (v, true) ≠ l.negate
v_in_c_del_l : (v, true) ∈ c.toList
h✝ : ¬v = l.fst
⊢ p v = true

Tactic:
next hne =>
exact pv

Result:
no goals