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

State before:
α : Type
g : CNF α
⊢ (List.any g fun c => !List.isEmpty c) = true ↔ ∃ a, mem a g
Tactic:
simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_false_iff_exists_mem, mem,
  Clause.mem]
State after:
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) ↔ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)

State before:
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) ↔ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
Tactic:
constructor
State after:
case mp
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) → ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)

case mpr
α : Type
g : CNF α
⊢ (∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)) → ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x

State before:
case mp
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) → ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)

case mpr
α : Type
g : CNF α
⊢ (∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)) → ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
Tactic:
. intro h
  rcases h with ⟨clause, ⟨hclause1, hclause2⟩⟩
  rcases hclause2 with ⟨lit, hlit⟩
  exists lit.fst, clause
  constructor
  . assumption
  . rcases lit with ⟨_, ⟨_ | _⟩⟩ <;> simp_all
State after:
case mpr
α : Type
g : CNF α
⊢ (∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)) → ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x

State before:
case mpr
α : Type
g : CNF α
⊢ (∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)) → ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
Tactic:
. intro h
  rcases h with ⟨lit, clause, ⟨hclause1, hclause2⟩⟩
  exists clause
  constructor
  . assumption
  . cases hclause2 with
    | inl hl => exact Exists.intro _ hl
    | inr hr => exact Exists.intro _ hr
State after:
no goals

State before:
case mp
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) → ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
Tactic:
intro h
State after:
case mp
α : Type
g : CNF α
h : ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)

State before:
case mp
α : Type
g : CNF α
h : ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
Tactic:
rcases h with ⟨clause, ⟨hclause1, hclause2⟩⟩
State after:
case mp.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : ∃ x, x ∈ clause
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)

State before:
case mp.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : ∃ x, x ∈ clause
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
Tactic:
rcases hclause2 with ⟨lit, hlit⟩
State after:
case mp.intro.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)

State before:
case mp.intro.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
Tactic:
exists lit.fst, clause
State after:
case mp.intro.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ clause ∈ g ∧ ((lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause)

State before:
case mp.intro.intro.intro
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ clause ∈ g ∧ ((lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause)
Tactic:
constructor
State after:
case mp.intro.intro.intro.left
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ clause ∈ g

case mp.intro.intro.intro.right
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ (lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause

State before:
case mp.intro.intro.intro.left
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ clause ∈ g

case mp.intro.intro.intro.right
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ (lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause
Tactic:
. assumption
State after:
case mp.intro.intro.intro.right
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ (lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause

State before:
case mp.intro.intro.intro.right
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ (lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause
Tactic:
. rcases lit with ⟨_, ⟨_ | _⟩⟩ <;> simp_all
State after:
no goals

State before:
case mp.intro.intro.intro.left
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ clause ∈ g
Tactic:
assumption
State after:
no goals

State before:
case mp.intro.intro.intro.right
α : Type
g : CNF α
clause : Clause α
hclause1 : clause ∈ g
lit : α × Bool
hlit : lit ∈ clause
⊢ (lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause
Tactic:
rcases lit with ⟨_, ⟨_ | _⟩⟩ <;> simp_all
State after:
no goals

State before:
case mpr
α : Type
g : CNF α
⊢ (∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)) → ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
Tactic:
intro h
State after:
case mpr
α : Type
g : CNF α
h : ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
⊢ ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x

State before:
case mpr
α : Type
g : CNF α
h : ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
⊢ ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
Tactic:
rcases h with ⟨lit, clause, ⟨hclause1, hclause2⟩⟩
State after:
case mpr.intro.intro.intro
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x

State before:
case mpr.intro.intro.intro
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x
Tactic:
exists clause
State after:
case mpr.intro.intro.intro
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ g ∧ ∃ x, x ∈ clause

State before:
case mpr.intro.intro.intro
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ g ∧ ∃ x, x ∈ clause
Tactic:
constructor
State after:
case mpr.intro.intro.intro.left
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ g

case mpr.intro.intro.intro.right
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ clause

State before:
case mpr.intro.intro.intro.left
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ g

case mpr.intro.intro.intro.right
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ clause
Tactic:
. assumption
State after:
case mpr.intro.intro.intro.right
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ clause

State before:
case mpr.intro.intro.intro.right
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ clause
Tactic:
. cases hclause2 with
  | inl hl => exact Exists.intro _ hl
  | inr hr => exact Exists.intro _ hr
State after:
no goals

State before:
case mpr.intro.intro.intro.left
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ g
Tactic:
assumption
State after:
no goals

State before:
case mpr.intro.intro.intro.right
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ clause
Tactic:
cases hclause2 with
| inl hl => exact Exists.intro _ hl
| inr hr => exact Exists.intro _ hr
State after:
no goals

State before:
case mpr.intro.intro.intro.right.inl
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hl : (lit, false) ∈ clause
⊢ ∃ x, x ∈ clause
Tactic:
exact Exists.intro _ hl
State after:
no goals

State before:
case mpr.intro.intro.intro.right.inr
α : Type
g : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ g
hr : (lit, true) ∈ clause
⊢ ∃ x, x ∈ clause
Tactic:
exact Exists.intro _ hr
State after:
no goals