Theorem: LRAT.DefaultClause.delete_iff (LeanSAT/LRAT/Clause.lean)

State before:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ (c.delete l).toList ↔ l' ≠ l ∧ l' ∈ c.toList
Tactic:
simp only [toList, delete, ne_eq]
State after:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause

State before:
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
by_cases hl : l' = l
State after:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause

State before:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause

case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
. simp only [hl, not_true, false_and, iff_false]
  exact List.Nodup.not_mem_erase c.nodup
State after:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause

State before:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
. simp only [hl, not_false_eq_true, true_and]
  exact List.mem_erase_of_ne hl
State after:
no goals

State before:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
simp only [hl, not_true, false_and, iff_false]
State after:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ ¬l ∈ c.clause.erase l

State before:
case pos
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : l' = l
⊢ ¬l ∈ c.clause.erase l
Tactic:
exact List.Nodup.not_mem_erase c.nodup
State after:
no goals

State before:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ ¬l' = l ∧ l' ∈ c.clause
Tactic:
simp only [hl, not_false_eq_true, true_and]
State after:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ l' ∈ c.clause

State before:
case neg
n : Nat
c : DefaultClause n
l l' : Literal (PosFin n)
hl : ¬l' = l
⊢ l' ∈ c.clause.erase l ↔ l' ∈ c.clause
Tactic:
exact List.mem_erase_of_ne hl
State after:
no goals