-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem any_not_isEmpty_iff_exists_mem {f : CNF α} :
    (List.any f fun c => !List.isEmpty c) = true ↔ ∃ v, Mem v f

Proof state:
case mp.intro.intro.intro.right
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
lit : Literal α
hlit : lit ∈ clause
⊢ (lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause

Tactic:
rcases lit with ⟨_, ⟨_ | _⟩⟩ <;> simp_all

Result:
no goals

Proof state:
case mpr.intro.intro.intro
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x

Tactic:
exists clause

Result:
case mpr.intro.intro.intro
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ f ∧ ∃ x, x ∈ clause

Proof state:
case mp
α : Type u_1
f : CNF α
h : ∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x
⊢ ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Tactic:
rcases h with ⟨clause, ⟨hclause1, hclause2⟩⟩

Result:
case mp.intro.intro
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
hclause2 : ∃ x, x ∈ clause
⊢ ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Proof state:
case mp.intro.intro.intro
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
lit : Literal α
hlit : lit ∈ clause
⊢ ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Tactic:
exists lit.fst, clause

Result:
case mp.intro.intro.intro
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
lit : Literal α
hlit : lit ∈ clause
⊢ clause ∈ f ∧ ((lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause)

Proof state:
case mp.intro.intro.intro
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
lit : Literal α
hlit : lit ∈ clause
⊢ clause ∈ f ∧ ((lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause)

Tactic:
constructor

Result:
case mp.intro.intro.intro.left
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
lit : Literal α
hlit : lit ∈ clause
⊢ clause ∈ f

case mp.intro.intro.intro.right
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
lit : Literal α
hlit : lit ∈ clause
⊢ (lit.fst, false) ∈ clause ∨ (lit.fst, true) ∈ clause

Proof state:
α : Type u_1
f : CNF α
⊢ (∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x) ↔ ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Tactic:
constructor

Result:
case mp
α : Type u_1
f : CNF α
⊢ (∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x) → ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

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

Proof state:
case mpr.intro.intro.intro
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ f ∧ ∃ x, x ∈ clause

Tactic:
constructor

Result:
case mpr.intro.intro.intro.left
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ f

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

Proof state:
case mpr.intro.intro.intro.right.inr
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
hr : (lit, true) ∈ clause
⊢ ∃ x, x ∈ clause

Tactic:
exact Exists.intro _ hr

Result:
no goals

Proof state:
case mpr.intro.intro.intro.left
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ clause ∈ f

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
f : CNF α
⊢ (List.any f fun c => !List.isEmpty c) = true ↔ ∃ v, Mem v f

Tactic:
simp only [List.any_eq_true, Bool.not_eq_true', List.isEmpty_eq_false_iff_exists_mem, Mem,
  Clause.Mem]

Result:
α : Type u_1
f : CNF α
⊢ (∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x) ↔ ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Proof state:
case mpr.intro.intro.intro.right.inl
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
hl : (lit, false) ∈ clause
⊢ ∃ x, x ∈ clause

Tactic:
exact Exists.intro _ hl

Result:
no goals

Proof state:
case mpr.intro.intro.intro.right
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
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

Result:
no goals

Proof state:
case mpr
α : Type u_1
f : CNF α
h : ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)
⊢ ∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x

Tactic:
rcases h with ⟨lit, clause, ⟨hclause1, hclause2⟩⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
f : CNF α
lit : α
clause : Clause α
hclause1 : clause ∈ f
hclause2 : (lit, false) ∈ clause ∨ (lit, true) ∈ clause
⊢ ∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x

Proof state:
case mp.intro.intro
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
hclause2 : ∃ x, x ∈ clause
⊢ ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Tactic:
rcases hclause2 with ⟨lit, hlit⟩

Result:
case mp.intro.intro.intro
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
lit : Literal α
hlit : lit ∈ clause
⊢ ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Proof state:
case mp.intro.intro.intro.left
α : Type u_1
f : CNF α
clause : Clause α
hclause1 : clause ∈ f
lit : Literal α
hlit : lit ∈ clause
⊢ clause ∈ f

Tactic:
assumption

Result:
no goals

Proof state:
case mp
α : Type u_1
f : CNF α
⊢ (∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x) → ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Tactic:
intro h

Result:
case mp
α : Type u_1
f : CNF α
h : ∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x
⊢ ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)

Proof state:
case mpr
α : Type u_1
f : CNF α
⊢ (∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)) → ∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x

Tactic:
intro h

Result:
case mpr
α : Type u_1
f : CNF α
h : ∃ v c, c ∈ f ∧ ((v, false) ∈ c ∨ (v, true) ∈ c)
⊢ ∃ x, x ∈ f ∧ ∃ x_1, x_1 ∈ x