-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/CNF.lean
theorem entails_of_entails_delete [DecidableEq α] [Clause α β] {p : α → Bool} {c : β}
    {l : Literal α} :
    p ⊨ delete c l → p ⊨ c

Proof state:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h2 : p v = true
h1 : ¬(v, true) = l ∧ (v, true) ∈ toList c
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true

Tactic:
exact Exists.intro v <| Or.inr ⟨h1.2, h2⟩

Result:
no goals

Proof state:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, true) ∈ toList (delete c l)
h2 : p v = true
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true

Tactic:
simp only [delete_iff, ne_eq] at h1

Result:
case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h2 : p v = true
h1 : ¬(v, true) = l ∧ (v, true) ∈ toList c
⊢ ∃ 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 α β
p : α → Bool
c : β
l : Literal α
⊢ p ⊨ delete c l → p ⊨ c

Tactic:
intro h

Result:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
h : p ⊨ delete c l
⊢ p ⊨ c

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

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

Result:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, false) ∈ toList (delete c l)
h2 : p v = false
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true

case intro.inr.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, true) ∈ toList (delete c l)
h2 : p v = true
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true

Proof state:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h2 : p v = false
h1 : ¬(v, false) = l ∧ (v, false) ∈ toList c
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true

Tactic:
exact Exists.intro v <| Or.inl ⟨h1.2, h2⟩

Result:
no goals

Proof state:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h1 : (v, false) ∈ toList (delete c l)
h2 : p v = false
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true

Tactic:
simp only [delete_iff, ne_eq] at h1

Result:
case intro.inl.intro
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
v : α
h2 : p v = false
h1 : ¬(v, false) = l ∧ (v, false) ∈ toList c
⊢ ∃ a, (a, false) ∈ toList c ∧ p a = false ∨ (a, true) ∈ toList c ∧ p a = true