Theorem: CNF.mem_append (LeanSAT/Reflect/CNF/Basic.lean)

State before:
α : Type
a : α
x y : CNF α
⊢ mem a (x ++ y) ↔ mem a x ∨ mem a y
Tactic:
simp [mem, List.mem_append]
State after:
α : Type
a : α
x y : CNF α
⊢ (∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c) ↔ (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c

State before:
α : Type
a : α
x y : CNF α
⊢ (∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c) ↔ (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c
Tactic:
constructor
State after:
case mp
α : Type
a : α
x y : CNF α
⊢ (∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c) → (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c

case mpr
α : Type
a : α
x y : CNF α
⊢ ((∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c) → ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c

State before:
case mp
α : Type
a : α
x y : CNF α
⊢ (∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c) → (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c
Tactic:
rintro ⟨c, (mx | my), mc⟩
State after:
case mp.intro.intro.inl
α : Type
a : α
x y : CNF α
c : Clause α
mc : Clause.mem a c
mx : c ∈ x
⊢ (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c

case mp.intro.intro.inr
α : Type
a : α
x y : CNF α
c : Clause α
mc : Clause.mem a c
my : c ∈ y
⊢ (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c

State before:
case mp.intro.intro.inl
α : Type
a : α
x y : CNF α
c : Clause α
mc : Clause.mem a c
mx : c ∈ x
⊢ (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c
Tactic:
left
State after:
case mp.intro.intro.inl.h
α : Type
a : α
x y : CNF α
c : Clause α
mc : Clause.mem a c
mx : c ∈ x
⊢ ∃ c, c ∈ x ∧ Clause.mem a c

State before:
case mp.intro.intro.inl.h
α : Type
a : α
x y : CNF α
c : Clause α
mc : Clause.mem a c
mx : c ∈ x
⊢ ∃ c, c ∈ x ∧ Clause.mem a c
Tactic:
exact ⟨c, mx, mc⟩
State after:
no goals

State before:
case mp.intro.intro.inr
α : Type
a : α
x y : CNF α
c : Clause α
mc : Clause.mem a c
my : c ∈ y
⊢ (∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c
Tactic:
right
State after:
case mp.intro.intro.inr.h
α : Type
a : α
x y : CNF α
c : Clause α
mc : Clause.mem a c
my : c ∈ y
⊢ ∃ c, c ∈ y ∧ Clause.mem a c

State before:
case mp.intro.intro.inr.h
α : Type
a : α
x y : CNF α
c : Clause α
mc : Clause.mem a c
my : c ∈ y
⊢ ∃ c, c ∈ y ∧ Clause.mem a c
Tactic:
exact ⟨c, my, mc⟩
State after:
no goals

State before:
case mpr
α : Type
a : α
x y : CNF α
⊢ ((∃ c, c ∈ x ∧ Clause.mem a c) ∨ ∃ c, c ∈ y ∧ Clause.mem a c) → ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c
Tactic:
rintro (⟨c, mx, mc⟩ | ⟨c, my, mc⟩)
State after:
case mpr.inl.intro.intro
α : Type
a : α
x y : CNF α
c : Clause α
mx : c ∈ x
mc : Clause.mem a c
⊢ ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c

case mpr.inr.intro.intro
α : Type
a : α
x y : CNF α
c : Clause α
my : c ∈ y
mc : Clause.mem a c
⊢ ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c

State before:
case mpr.inl.intro.intro
α : Type
a : α
x y : CNF α
c : Clause α
mx : c ∈ x
mc : Clause.mem a c
⊢ ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c
Tactic:
exact ⟨c, Or.inl mx, mc⟩
State after:
no goals

State before:
case mpr.inr.intro.intro
α : Type
a : α
x y : CNF α
c : Clause α
my : c ∈ y
mc : Clause.mem a c
⊢ ∃ c, (c ∈ x ∨ c ∈ y) ∧ Clause.mem a c
Tactic:
exact ⟨c, Or.inr my, mc⟩
State after:
no goals