Theorem: LRAT.Clause.entails_of_entails_delete (LeanSAT/LRAT/CNF.lean)

State before:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
⊢ p ⊨ delete c l → p ⊨ c
Tactic:
intro h
State after:
α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Clause α β
p : α → Bool
c : β
l : Literal α
h : p ⊨ delete c l
⊢ p ⊨ c

State before:
α : 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⟩⟩
State after:
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

State before:
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
Tactic:
. simp only [delete_iff, ne_eq] at h1
  exact Exists.intro v $ Or.inl ⟨h1.2, h2⟩
State after:
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

State before:
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
  exact Exists.intro v $ Or.inr ⟨h1.2, h2⟩
State after:
no goals

State before:
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
State after:
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

State before:
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⟩
State after:
no goals

State before:
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
State after:
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

State before:
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⟩
State after:
no goals