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

Tactic:
apply Or.inr

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

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

Tactic:
next v_ne_l =>
simp only [decide_eq_false_iff_not] at h2
exfalso
exact h2 h1

Result:
no goals

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

Tactic:
rcases h with ⟨v, ⟨h1, h2⟩ | ⟨h1, h2⟩⟩

Result:
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 : p ⊨ (v, false)
⊢ l ∈ toList c

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 : p ⊨ (v, true)
⊢ l ∈ 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, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))

Tactic:
exact ⟨h, pl⟩

Result:
no goals

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

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

case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ l ∈ toList 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))

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

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

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 = false
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false))

Tactic:
rw [← 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, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ l ∈ toList 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))

Tactic:
intro h p pl

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
⊢ ∃ a, (a, false) ∈ toList c ∧ (p ⊨ (a, false)) ∨ (a, true) ∈ toList c ∧ (p ⊨ (a, true))

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 : ¬(v, false) ∈ toList c
⊢ False

Tactic:
exact h2 h1

Result:
no goals

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 = false
⊢ (l.fst, l.snd) ∈ toList c ∧ (p ⊨ (l.fst, l.snd))

Tactic:
exact ⟨h, pl⟩

Result:
no goals

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

Tactic:
next v_eq_l =>
cases l
simp_all

Result:
no goals

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
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

Tactic:
by_cases hl : l.2

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

case neg
α : 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)) ∨ (l.fst, true) ∈ toList c ∧ (p ⊨ (l.fst, true))

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

Tactic:
apply Or.inl

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 = true
⊢ (l.fst, false) ∈ toList c ∧ (p ⊨ (l.fst, false))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
l : Literal α
c : β
⊢ Limplies α l c ↔ l ∈ toList c

Tactic:
simp only [Limplies, sat_iff_exists, Prod.exists, Bool.exists_bool]

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