-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem not_exists_mem : (¬ ∃ v, Mem v f) ↔ ∃ n, f = List.replicate n []

Proof state:
α✝ : Type u_1
f : CNF α✝
⊢ (¬∃ v, Mem v f) ↔ ∃ n, f = List.replicate n []

Tactic:
simp only [← any_not_isEmpty_iff_exists_mem]

Result:
α✝ : Type u_1
f : CNF α✝
⊢ ¬(List.any f fun c => !List.isEmpty c) = true ↔ ∃ n, f = List.replicate n []

Proof state:
case cons
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → List.isEmpty x = true) ↔ ∃ n, f = List.replicate n []
⊢ (∀ (x : Clause α✝), x ∈ c :: f → List.isEmpty x = true) ↔ ∃ n, c :: f = List.replicate n []

Tactic:
simp_all [ih, List.isEmpty_iff]

Result:
case cons
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
⊢ (c = [] ∧ ∃ n, f = List.replicate n []) ↔ ∃ n, c :: f = List.replicate n []

Proof state:
case cons.mpr.intro.succ
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
n✝ : Nat
ih : (∀ (x : Clause α✝), x ∈ List.replicate n✝ [] → x = []) ↔ ∃ n, List.replicate n✝ [] = List.replicate n []
h : c = [] ∧ f = List.replicate n✝ []
⊢ ∃ n, List.replicate n✝ [] = List.replicate n []

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
case cons.mpr.intro.succ
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
n✝ : Nat
h : c :: f = List.replicate (n✝ + 1) []
⊢ c = [] ∧ ∃ n, f = List.replicate n []

Tactic:
simp_all only [List.replicate, List.cons.injEq, true_and]

Result:
case cons.mpr.intro.succ
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
n✝ : Nat
ih : (∀ (x : Clause α✝), x ∈ List.replicate n✝ [] → x = []) ↔ ∃ n, List.replicate n✝ [] = List.replicate n []
h : c = [] ∧ f = List.replicate n✝ []
⊢ ∃ n, List.replicate n✝ [] = List.replicate n []

Proof state:
case cons.mpr.intro
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
n : Nat
h : c :: f = List.replicate n []
⊢ c = [] ∧ ∃ n, f = List.replicate n []

Tactic:
cases n

Result:
case cons.mpr.intro.zero
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
h : c :: f = List.replicate 0 []
⊢ c = [] ∧ ∃ n, f = List.replicate n []

case cons.mpr.intro.succ
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
n✝ : Nat
h : c :: f = List.replicate (n✝ + 1) []
⊢ c = [] ∧ ∃ n, f = List.replicate n []

Proof state:
case cons.mpr
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
⊢ (∃ n, c :: f = List.replicate n []) → c = [] ∧ ∃ n, f = List.replicate n []

Tactic:
rintro ⟨n, h⟩

Result:
case cons.mpr.intro
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
n : Nat
h : c :: f = List.replicate n []
⊢ c = [] ∧ ∃ n, f = List.replicate n []

Proof state:
case nil
α✝ : Type u_1
⊢ (∀ (x : Clause α✝), x ∈ [] → List.isEmpty x = true) ↔ ∃ n, [] = List.replicate n []

Tactic:
simp only [List.not_mem_nil, List.isEmpty_iff, false_implies, forall_const, true_iff]

Result:
case nil
α✝ : Type u_1
⊢ ∃ n, [] = List.replicate n []

Proof state:
case cons.mp.intro.intro
α✝ : Type u_1
n : Nat
ih : (∀ (x : Clause α✝), x ∈ List.replicate n [] → x = []) ↔ ∃ n_1, List.replicate n [] = List.replicate n_1 []
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []

Tactic:
exact ⟨n+1, rfl⟩

Result:
no goals

Proof state:
α✝ : Type u_1
f : CNF α✝
⊢ ¬(List.any f fun c => !List.isEmpty c) = true ↔ ∃ n, f = List.replicate n []

Tactic:
simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false]

Result:
α✝ : Type u_1
f : CNF α✝
⊢ (∀ (x : Clause α✝), x ∈ f → List.isEmpty x = true) ↔ ∃ n, f = List.replicate n []

Proof state:
case cons
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
⊢ (c = [] ∧ ∃ n, f = List.replicate n []) ↔ ∃ n, c :: f = List.replicate n []

Tactic:
constructor

Result:
case cons.mp
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
⊢ (c = [] ∧ ∃ n, f = List.replicate n []) → ∃ n, c :: f = List.replicate n []

case cons.mpr
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
⊢ (∃ n, c :: f = List.replicate n []) → c = [] ∧ ∃ n, f = List.replicate n []

Proof state:
case nil
α✝ : Type u_1
⊢ ∃ n, [] = List.replicate n []

Tactic:
exact ⟨0, rfl⟩

Result:
no goals

Proof state:
case cons.mpr.intro.zero
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
h : c :: f = List.replicate 0 []
⊢ c = [] ∧ ∃ n, f = List.replicate n []

Tactic:
simp at h

Result:
no goals

Proof state:
case cons.mp
α✝ : Type u_1
c : Clause α✝
f : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ f → x = []) ↔ ∃ n, f = List.replicate n []
⊢ (c = [] ∧ ∃ n, f = List.replicate n []) → ∃ n, c :: f = List.replicate n []

Tactic:
rintro ⟨rfl, n, rfl⟩

Result:
case cons.mp.intro.intro
α✝ : Type u_1
n : Nat
ih : (∀ (x : Clause α✝), x ∈ List.replicate n [] → x = []) ↔ ∃ n_1, List.replicate n [] = List.replicate n_1 []
⊢ ∃ n_1, [] :: List.replicate n [] = List.replicate n_1 []