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

State before:
n : Nat
⊢ ∀ (c : DefaultClause n) (l : Literal (PosFin n)), c.contains l = true ↔ l ∈ c.toList
Tactic:
intro c l
State after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.contains l = true ↔ l ∈ c.toList

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ c.contains l = true ↔ l ∈ c.toList
Tactic:
simp only [contains, List.contains]
State after:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true ↔ l ∈ c.toList

State before:
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true ↔ l ∈ c.toList
Tactic:
constructor
State after:
case mp
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true → l ∈ c.toList

case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true

State before:
case mp
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true → l ∈ c.toList

case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true
Tactic:
. exact List.mem_of_elem_eq_true
State after:
case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true

State before:
case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true
Tactic:
. exact List.elem_eq_true_of_mem
State after:
no goals

State before:
case mp
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ List.elem l c.clause = true → l ∈ c.toList
Tactic:
exact List.mem_of_elem_eq_true
State after:
no goals

State before:
case mpr
n : Nat
c : DefaultClause n
l : Literal (PosFin n)
⊢ l ∈ c.toList → List.elem l c.clause = true
Tactic:
exact List.elem_eq_true_of_mem
State after:
no goals