-- 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:
α : 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 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c

Tactic:
simp only [decide_eq_true_eq] at h2

Result:
α : 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
⊢ l ∈ toList c

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
h : l ∈ toList c
p : α → Bool
pl : p ⊨ l
⊢ ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))

Tactic:
apply Exists.intro l.1

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

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ (∀ (a : α → Bool),
      a ⊨ l → ∃ a_2, (a_2, false) ∈ toList c ∧ (a ⊨ (a_2, false)) ∨ (a_2, true) ∈ toList c ∧ (a ⊨ (a_2, true))) →
    l ∈ toList c

Tactic:
intro h

Result:
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))
⊢ l ∈ toList c

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_eq_l : v = l.fst
h2 : l.snd = true
⊢ l ∈ toList c

Tactic:
cases l

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

Proof state:
case pos.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, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

Tactic:
rw [← hl]

Result:
case pos.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, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))

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, false) ∈ toList c
v_eq_l : v = l.fst
h2 : l.snd = false
⊢ l ∈ toList c

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
c : β
v : α
h1 : (v, false) ∈ 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 = false
⊢ (fst✝, snd✝) ∈ toList c

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

Tactic:
exact v_not_in_c h1

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, false) ∈ toList c
v_ne_l : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = false
⊢ l ∈ toList c

Tactic:
simp only [decide_eq_false_iff_not] at h2

Result:
α : 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
v_ne_l : ¬v = l.fst
h2 : ¬(v, false) ∈ toList c
⊢ l ∈ toList c

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 : ¬Literal.negate (v, true) ∈ toList c
⊢ False

Tactic:
simp only [Literal.negate, Bool.not_true] at negv_not_in_c

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

Proof state:
case mp.intro.inr.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, true) ∈ toList c
h2 : (if v = l.fst then l.snd else decide ((v, false) ∈ toList c)) = true
⊢ l ∈ toList c

Tactic:
split at h2

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

case mp.intro.inr.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, true) ∈ toList c
h✝ : ¬v = l.fst
h2 : decide ((v, false) ∈ toList c) = true
⊢ l ∈ toList c

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))
⊢ l ∈ toList c

Tactic:
let p := fun x : α => if x = l.1 then l.2 else (x, false) ∈ toList c

Result:
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)
⊢ l ∈ toList c

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
⊢ l ∈ toList c

Tactic:
exfalso

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