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

State before:
α✝ : Type
g : CNF α✝
⊢ (¬∃ a, mem a g) ↔ ∃ n, g = List.replicate n []
Tactic:
simp only [← any_nonEmpty_iff_exists_mem]
State after:
α✝ : Type
g : CNF α✝
⊢ ¬(List.any g fun c => !List.isEmpty c) = true ↔ ∃ n, g = List.replicate n []

State before:
α✝ : Type
g : CNF α✝
⊢ ¬(List.any g fun c => !List.isEmpty c) = true ↔ ∃ n, g = List.replicate n []
Tactic:
simp only [List.any_eq_true, Bool.not_eq_true', not_exists, not_and, Bool.not_eq_false]
State after:
α✝ : Type
g : CNF α✝
⊢ (∀ (x : Clause α✝), x ∈ g → List.isEmpty x = true) ↔ ∃ n, g = List.replicate n []

State before:
case nil
α✝ : Type
⊢ (∀ (x : Clause α✝), x ∈ [] → List.isEmpty x = true) ↔ ∃ n, [] = List.replicate n []
Tactic:
simp only [List.not_mem_nil, List.isEmpty_true_iff, false_implies, forall_const, true_iff]
State after:
case nil
α✝ : Type
⊢ ∃ n, [] = List.replicate n []

State before:
case nil
α✝ : Type
⊢ ∃ n, [] = List.replicate n []
Tactic:
exact ⟨0, rfl⟩
State after:
no goals

State before:
case cons
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → List.isEmpty x = true) ↔ ∃ n, g = List.replicate n []
⊢ (∀ (x : Clause α✝), x ∈ c :: g → List.isEmpty x = true) ↔ ∃ n, c :: g = List.replicate n []
Tactic:
simp_all [ih]
State after:
case cons
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
⊢ (c = [] ∧ ∃ n, g = List.replicate n []) ↔ ∃ n, c :: g = List.replicate n []

State before:
case cons
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
⊢ (c = [] ∧ ∃ n, g = List.replicate n []) ↔ ∃ n, c :: g = List.replicate n []
Tactic:
constructor
State after:
case cons.mp
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
⊢ (c = [] ∧ ∃ n, g = List.replicate n []) → ∃ n, c :: g = List.replicate n []

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

State before:
case cons.mp
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
⊢ (c = [] ∧ ∃ n, g = List.replicate n []) → ∃ n, c :: g = List.replicate n []
Tactic:
rintro ⟨rfl, n, rfl⟩
State after:
case cons.mp.intro.intro
α✝ : Type
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 []

State before:
case cons.mp.intro.intro
α✝ : Type
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⟩
State after:
no goals

State before:
case cons.mpr
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
⊢ (∃ n, c :: g = List.replicate n []) → c = [] ∧ ∃ n, g = List.replicate n []
Tactic:
rintro ⟨n, h⟩
State after:
case cons.mpr.intro
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
n : Nat
h : c :: g = List.replicate n []
⊢ c = [] ∧ ∃ n, g = List.replicate n []

State before:
case cons.mpr.intro
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
n : Nat
h : c :: g = List.replicate n []
⊢ c = [] ∧ ∃ n, g = List.replicate n []
Tactic:
cases n
State after:
case cons.mpr.intro.zero
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
h : c :: g = List.replicate 0 []
⊢ c = [] ∧ ∃ n, g = List.replicate n []

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

State before:
case cons.mpr.intro.zero
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
h : c :: g = List.replicate 0 []
⊢ c = [] ∧ ∃ n, g = List.replicate n []
Tactic:
simp at h
State after:
no goals

State before:
case cons.mpr.intro.succ
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
ih : (∀ (x : Clause α✝), x ∈ g → x = []) ↔ ∃ n, g = List.replicate n []
n✝ : Nat
h : c :: g = List.replicate (n✝ + 1) []
⊢ c = [] ∧ ∃ n, g = List.replicate n []
Tactic:
simp_all only [List.replicate, List.cons.injEq, true_and]
State after:
case cons.mpr.intro.succ
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
n✝ : Nat
ih : (∀ (x : Clause α✝), x ∈ List.replicate n✝ [] → x = []) ↔ ∃ n, List.replicate n✝ [] = List.replicate n []
h : c = [] ∧ g = List.replicate n✝ []
⊢ ∃ n, List.replicate n✝ [] = List.replicate n []

State before:
case cons.mpr.intro.succ
α✝ : Type
c : Clause α✝
g : List (Clause α✝)
n✝ : Nat
ih : (∀ (x : Clause α✝), x ∈ List.replicate n✝ [] → x = []) ↔ ∃ n, List.replicate n✝ [] = List.replicate n []
h : c = [] ∧ g = List.replicate n✝ []
⊢ ∃ n, List.replicate n✝ [] = List.replicate n []
Tactic:
exact ⟨_, rfl⟩
State after:
no goals