internlm/Lean-Github huggingface dataset:
Theorem: CNF.Clause.eval_congr
Proof state before:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ (f i.fst == i.snd || eval f c) = (g i.fst == i.snd || eval g c)
Tactic:
rw [ih, w]
Proof state after:
case a
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ mem i.fst (i :: c)

α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ ∀ (i : α), mem i c → f i = g i
Theorem: CNF.Clause.eval_congr
Proof state before:
case a
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ mem i.fst (i :: c)
Tactic:
rcases i with ⟨b, (_|_)⟩ <;> simp [mem]
Proof state after:
no goals
Theorem: CNF.Clause.eval_congr
Proof state before:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
⊢ ∀ (i : α), mem i c → f i = g i
Tactic:
intro j h
Proof state after:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : mem j c
⊢ f j = g j
Theorem: CNF.Clause.eval_congr
Proof state before:
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : mem j c
⊢ f j = g j
Tactic:
apply w
Proof state after:
case a
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : mem j c
⊢ mem j (i :: c)
Theorem: CNF.Clause.eval_congr
Proof state before:
case a
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : mem j c
⊢ mem j (i :: c)
Tactic:
rcases h with h | h
Proof state after:
case a.inl
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, false) ∈ c
⊢ mem j (i :: c)

case a.inr
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, true) ∈ c
⊢ mem j (i :: c)
Theorem: CNF.Clause.eval_congr
Proof state before:
case a.inl
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, false) ∈ c
⊢ mem j (i :: c)
Tactic:
left
Proof state after:
case a.inl.h
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, false) ∈ c
⊢ (j, false) ∈ i :: c
Theorem: CNF.Clause.eval_congr
Proof state before:
case a.inl.h
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, false) ∈ c
⊢ (j, false) ∈ i :: c
Tactic:
apply List.mem_cons_of_mem _ h
Proof state after:
no goals
Theorem: CNF.Clause.eval_congr
Proof state before:
case a.inr
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, true) ∈ c
⊢ mem j (i :: c)
Tactic:
right
Proof state after:
case a.inr.h
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, true) ∈ c
⊢ (j, true) ∈ i :: c
Theorem: CNF.Clause.eval_congr
Proof state before:
case a.inr.h
α : Type
f g : α → Bool
i : α × Bool
c : List (α × Bool)
ih : (∀ (i : α), mem i c → f i = g i) → eval f c = eval g c
w : ∀ (i_1 : α), mem i_1 (i :: c) → f i_1 = g i_1
j : α
h : (j, true) ∈ c
⊢ (j, true) ∈ i :: c
Tactic:
apply List.mem_cons_of_mem _ h
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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]
Proof state after:
α : Type
g : CNF α
⊢ (∃ x, x ∈ g ∧ ∃ x_1, x_1 ∈ x) ↔ ∃ a c, c ∈ g ∧ ((a, false) ∈ c ∨ (a, true) ∈ c)
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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)
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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⟩⟩
Proof 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)
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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⟩
Proof 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)
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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)
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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⟩⟩
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof 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
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.any_nonEmpty_iff_exists_mem
Proof 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
Proof state after:
no goals
Theorem: CNF.not_mem_cons
Proof state before:
α✝ : Type
g : CNF α✝
⊢ (¬∃ a, mem a g) ↔ ∃ n, g = List.replicate n []
Tactic:
simp only [← any_nonEmpty_iff_exists_mem]
Proof state after:
α✝ : Type
g : CNF α✝
⊢ ¬(List.any g fun c => !List.isEmpty c) = true ↔ ∃ n, g = List.replicate n []
Theorem: CNF.not_mem_cons
Proof 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]
Proof state after:
α✝ : Type
g : CNF α✝
⊢ (∀ (x : Clause α✝), x ∈ g → List.isEmpty x = true) ↔ ∃ n, g = List.replicate n []
Theorem: CNF.not_mem_cons
Proof 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]
Proof state after:
case nil
α✝ : Type
⊢ ∃ n, [] = List.replicate n []
Theorem: CNF.not_mem_cons
Proof state before:
case nil
α✝ : Type
⊢ ∃ n, [] = List.replicate n []
Tactic:
exact ⟨0, rfl⟩
Proof state after:
no goals
Theorem: CNF.not_mem_cons
Proof 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]
Proof 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 []
Theorem: CNF.not_mem_cons
Proof 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
Proof 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 []
Theorem: CNF.not_mem_cons
Proof 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⟩
Proof 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 []
Theorem: CNF.not_mem_cons
Proof 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⟩
Proof state after:
no goals
Theorem: CNF.not_mem_cons
Proof 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⟩
Proof 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 []
Theorem: CNF.not_mem_cons
Proof 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
Proof 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 []
Theorem: CNF.not_mem_cons
Proof 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
Proof state after:
no goals
Theorem: CNF.not_mem_cons
Proof 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]
Proof 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 []
Theorem: CNF.not_mem_cons
Proof 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⟩
Proof state after:
no goals
Theorem: CNF.not_mem_nil
Proof state before:
α : Type
a : α
⊢ mem a [] ↔ False
Tactic:
simp [mem]
Proof state after:
no goals
Theorem: CNF.mem_cons
Proof state before:
α : Type
a : α
i : Clause α
c : CNF α
⊢ mem a (i :: c) ↔ Clause.mem a i ∨ mem a c
Tactic:
simp [mem]
Proof state after:
no goals
Theorem: CNF.mem_of
Proof state before:
α✝ : Type
c : Clause α✝
g : CNF α✝
a : α✝
h : c ∈ g
w : Clause.mem a c
⊢ mem a g
Tactic:
apply Exists.intro c
Proof state after:
α✝ : Type
c : Clause α✝
g : CNF α✝
a : α✝
h : c ∈ g
w : Clause.mem a c
⊢ c ∈ g ∧ Clause.mem a c
Theorem: CNF.mem_of
Proof state before:
α✝ : Type
c : Clause α✝
g : CNF α✝
a : α✝
h : c ∈ g
w : Clause.mem a c
⊢ c ∈ g ∧ Clause.mem a c
Tactic:
constructor <;> assumption
Proof state after:
no goals
Theorem: CNF.mem_append
Proof state before:
α : Type
a : α
x y : CNF α
⊢ mem a (x ++ y) ↔ mem a x ∨ mem a y
Tactic:
simp [mem, List.mem_append]
Proof 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
Theorem: CNF.mem_append
Proof 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
Proof 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
Theorem: CNF.mem_append
Proof 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⟩
Proof 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
Theorem: CNF.mem_append
Proof 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
Proof 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
Theorem: CNF.mem_append
Proof 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⟩
Proof state after:
no goals
Theorem: CNF.mem_append
Proof 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
Proof 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
Theorem: CNF.mem_append
Proof 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⟩
Proof state after:
no goals
Theorem: CNF.mem_append
Proof 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⟩)
Proof 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
Theorem: CNF.mem_append
Proof 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⟩
Proof state after:
no goals
Theorem: CNF.mem_append
Proof 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⟩
Proof state after:
no goals