-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem limplies_iff_mem [DecidableEq α] [Clause α β] (l : Literal α) (c : β) :
    Limplies α l c ↔ l ∈ toList c

Proof state:
case neg.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : ¬l.snd = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false))

Tactic:
simp only [Bool.not_eq_true] at hl

Result:
case neg.h
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
hl : l.snd = false
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false))

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬(v, false) ∈ toList c
⊢ False

Tactic:
exact negv_not_in_c h2

Result:
no goals

Proof state:
case mp.intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h2 : (if v = l.fst then l.snd else decide ((v, false) ∈ toList c)) = false
⊢ l ∈ toList c

Tactic:
split at h2

Result:
case mp.intro.inl.intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : v = l.fst
h2 : l.snd = false
⊢ l ∈ toList c

case mp.intro.inl.intro.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, false) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = false
⊢ l ∈ toList c

Proof state:
case mp.intro.inr.intro.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
h✝ : v = l.fst
h2 : l.snd = true
⊢ l ∈ toList c

Tactic:
next v_eq_l =>
cases l
simp_all

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
c : β
v : α
h1 : (v, true) ∈ toList c
fst✝ : α
snd✝ : Bool
p : α → Bool := fun x => if x = (fst✝, snd✝).fst then (fst✝, snd✝).snd else decide ((x, false) ∈ toList c)
pl : p ⊨ (fst✝, snd✝)
v_eq_l : v = (fst✝, snd✝).fst
h2 : (fst✝, snd✝).snd = true
⊢ (fst✝, snd✝) ∈ toList c

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
⊢ False

Tactic:
rcases not_tautology c (v, true) with v_not_in_c | negv_not_in_c

Result:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
v_not_in_c : ¬(v, true) ∈ toList c
⊢ False

case inr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
v : α
h1 : (v, true) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : (v, false) ∈ toList c
negv_not_in_c : ¬Literal.negate (v, true) ∈ toList c
⊢ False

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h :
  ∀ (a : α → Bool),
    a ⊨ l → ∃ a_2, (a_2, false) ∈ toList c ∧ (a ⊨ (a_2, false)) ∨ (a_2, true) ∈ toList c ∧ (a ⊨ (a_2, true))
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
⊢ l ∈ toList c

Tactic:
specialize h p pl

Result:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
p : α → Bool := fun x => if x = l.fst then l.snd else decide ((x, false) ∈ toList c)
pl : p ⊨ l
h : ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))
⊢ l ∈ toList c