Theorem: CNF.Clause.mem_cons (LeanSAT/Reflect/CNF/Basic.lean)

State before:
α : Type
i : α × Bool
c : List (α × Bool)
a : α
⊢ mem a (i :: c) ↔ a = i.fst ∨ mem a c
Tactic:
rcases i with ⟨b, (_|_)⟩
State after:
case mk.false
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, false) :: c) ↔ a = (b, false).fst ∨ mem a c

case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, true) :: c) ↔ a = (b, true).fst ∨ mem a c

State before:
case mk.false
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, false) :: c) ↔ a = (b, false).fst ∨ mem a c
Tactic:
simp [mem, or_assoc]
State after:
no goals

State before:
case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ mem a ((b, true) :: c) ↔ a = (b, true).fst ∨ mem a c
Tactic:
simp [mem]
State after:
case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ (a, false) ∈ c ∨ a = b ∨ (a, true) ∈ c ↔ a = b ∨ (a, false) ∈ c ∨ (a, true) ∈ c

State before:
case mk.true
α : Type
c : List (α × Bool)
a b : α
⊢ (a, false) ∈ c ∨ a = b ∨ (a, true) ∈ c ↔ a = b ∨ (a, false) ∈ c ∨ (a, true) ∈ c
Tactic:
rw [or_left_comm]
State after:
no goals