-- 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.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

Tactic:
next heq =>
simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
simp_all

Result:
no goals

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
heq : v = l.fst
⊢ l.snd = true

Tactic:
simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v

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

Proof state:
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

Tactic:
split

Result:
case intro.inr.intro.intro.h.right.isTrue
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
⊢ l.snd = true

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

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
heq : v = l.fst
⊢ l.snd = false

Tactic:
simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v

Result:
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

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

Tactic:
simp_all

Result:
no goals

Proof state:
case intro.inl.intro.intro.h
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

Tactic:
constructor

Result:
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)

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

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
⊢ (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:
left

Result:
case intro.inl.intro.intro.h
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

Proof state:
case intro.inr.intro.intro.h.right.isTrue
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
⊢ l.snd = true

Tactic:
next heq =>
simp only [heq, Literal.negate, ne_eq, Prod.mk.injEq, true_and] at negl_ne_v
simp_all

Result:
no goals