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

State before:
α✝ : Type
a : α✝
b : Bool
c : Clause α✝
h : (a, b) ∈ c
⊢ mem a c
Tactic:
cases b
State after:
case false
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ mem a c

case true
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ mem a c

State before:
case false
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ mem a c
Tactic:
left
State after:
case false.h
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ (a, false) ∈ c

State before:
case false.h
α✝ : Type
a : α✝
c : Clause α✝
h : (a, false) ∈ c
⊢ (a, false) ∈ c
Tactic:
exact h
State after:
no goals

State before:
case true
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ mem a c
Tactic:
right
State after:
case true.h
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ (a, true) ∈ c

State before:
case true.h
α✝ : Type
a : α✝
c : Clause α✝
h : (a, true) ∈ c
⊢ (a, true) ∈ c
Tactic:
exact h
State after:
no goals