internlm/Lean-Github huggingface dataset:
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : x ∈ W ∩ X ∧ f x = y
⊢ y ∈ image f W ∩ image f X
Tactic:
define : x ∈ W ∩ X at h2
Proof state after:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f W ∩ image f X
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f W ∩ image f X
Tactic:
apply And.intro
Proof state after:
case left
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f W

case right
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f X
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
case left
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f W
Tactic:
define
Proof state after:
case left
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ ∃ x ∈ W, f x = y
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
case left
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ ∃ x ∈ W, f x = y
Tactic:
show ∃ (x : A), x ∈ W ∧ f x = y from
  Exists.intro x (And.intro h2.left.left h2.right)
Proof state after:
no goals
Theorem: HTPI.Theorem_5_5_2_1
Proof state before:
case right
A B : Type
f : A → B
W X : Set A
y : B
h1 : ∃ x ∈ W ∩ X, f x = y
x : A
h2 : (x ∈ W ∧ x ∈ X) ∧ f x = y
⊢ y ∈ image f X
Tactic:
show y ∈ image f X from
  Exists.intro x (And.intro h2.left.right h2.right)
Proof state after:
no goals
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
⊢ image f (W ∩ X) = image f W ∩ image f X
Tactic:
apply Set.ext
Proof state after:
case h
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
⊢ ∀ (x : B), x ∈ image f (W ∩ X) ↔ x ∈ image f W ∩ image f X
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
⊢ ∀ (x : B), x ∈ image f (W ∩ X) ↔ x ∈ image f W ∩ image f X
Tactic:
fix y : B
Proof state after:
case h
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f (W ∩ X) ↔ y ∈ image f W ∩ image f X
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f (W ∩ X) ↔ y ∈ image f W ∩ image f X
Tactic:
apply Iff.intro
Proof state after:
case h.mp
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f (W ∩ X) → y ∈ image f W ∩ image f X

case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f W ∩ image f X → y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mp
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f (W ∩ X) → y ∈ image f W ∩ image f X
Tactic:
assume h2 : y ∈ image f (W ∩ X)
Proof state after:
case h.mp
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f (W ∩ X)
⊢ y ∈ image f W ∩ image f X
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mp
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f (W ∩ X)
⊢ y ∈ image f W ∩ image f X
Tactic:
show y ∈ image f W ∩ image f X from Theorem_5_5_2_1 f W X h2
Proof state after:
no goals
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
⊢ y ∈ image f W ∩ image f X → y ∈ image f (W ∩ X)
Tactic:
assume h2 : y ∈ image f W ∩ image f X
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f W ∩ image f X
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f W ∩ image f X
⊢ y ∈ image f (W ∩ X)
Tactic:
define at h2
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f W ∧ y ∈ image f X
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : y ∈ image f W ∧ y ∈ image f X
⊢ y ∈ image f (W ∩ X)
Tactic:
rewrite [image_def, image_def] at h2
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
⊢ y ∈ image f (W ∩ X)
Tactic:
obtain (x1 : A) (h3 : x1 ∈ W ∧ f x1 = y) from h2.left
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
⊢ y ∈ image f (W ∩ X)
Tactic:
obtain (x2 : A) (h4 : x2 ∈ X ∧ f x2 = y) from h2.right
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
⊢ y ∈ image f (W ∩ X)
Tactic:
have h5 : f x2 = y := h4.right
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = y
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = y
⊢ y ∈ image f (W ∩ X)
Tactic:
rewrite [←h3.right] at h5
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : one_to_one f
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
⊢ y ∈ image f (W ∩ X)
Tactic:
define at h1
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
⊢ y ∈ image f (W ∩ X)
Tactic:
have h6 : x2 = x1 := h1 x2 x1 h5
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
h6 : x2 = x1
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x2 ∈ X ∧ f x2 = y
h5 : f x2 = f x1
h6 : x2 = x1
⊢ y ∈ image f (W ∩ X)
Tactic:
rewrite [h6] at h4
Proof state after:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x1 ∈ X ∧ f x1 = y
h5 : f x2 = f x1
h6 : x2 = x1
⊢ y ∈ image f (W ∩ X)
Theorem: HTPI.Theorem_5_5_2_2
Proof state before:
case h.mpr
A B : Type
f : A → B
W X : Set A
h1 : ∀ (x1 x2 : A), f x1 = f x2 → x1 = x2
y : B
h2 : (∃ x ∈ W, f x = y) ∧ ∃ x ∈ X, f x = y
x1 : A
h3 : x1 ∈ W ∧ f x1 = y
x2 : A
h4 : x1 ∈ X ∧ f x1 = y
h5 : f x2 = f x1
h6 : x2 = x1
⊢ y ∈ image f (W ∩ X)
Tactic:
show y ∈ image f (W ∩ X) from
  Exists.intro x1 (And.intro (And.intro h3.left h4.left) h3.right)
Proof state after:
no goals
Theorem: clauseContains_trans
Proof state before:
n : ℕ
cl1 cl2 cl3 : Clause n
⊢ cl1⊇cl2 → cl2⊇cl3 → cl1⊇cl3
Tactic:
intro hyp1 hyp2  k w b dHyp
Proof state after:
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl1 k w = some b
Theorem: clauseContains_trans
Proof state before:
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl1 k w = some b
Tactic:
apply hyp1
Proof state after:
case a
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl2 k w = some b
Theorem: clauseContains_trans
Proof state before:
case a
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl2 k w = some b
Tactic:
apply hyp2
Proof state after:
case a.a
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl3 k w = some b
Theorem: clauseContains_trans
Proof state before:
case a.a
n : ℕ
cl1 cl2 cl3 : Clause n
hyp1 : cl1⊇cl2
hyp2 : cl2⊇cl3
k : ℕ
w : k < n
b : Bool
dHyp : get' cl3 k w = some b
⊢ get' cl3 k w = some b
Tactic:
apply dHyp
Proof state after:
no goals
Theorem: clauseContains_prepend
Proof state before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
⊢ v1 ≥ v2 → cl1⊇cl2 → v1 ::ᵥ cl1⊇v2 ::ᵥ cl2
Tactic:
intro hyp1 hyp2 k
Proof state after:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
⊢ ∀ (kw : k < succ n) (b : Bool), get' (v2 ::ᵥ cl2) k kw = some b → get' (v1 ::ᵥ cl1) k kw = some b
Theorem: clauseContains_prepend
Proof state before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
⊢ ∀ (kw : k < succ n) (b : Bool), get' (v2 ::ᵥ cl2) k kw = some b → get' (v1 ::ᵥ cl1) k kw = some b
Tactic:
match k with
| zero =>
  intro w b hb
  exact hyp1 b hb
| j + 1  =>
  intro kw b hb
  have w : j < n := by
      apply le_of_succ_le_succ
      exact kw
  exact hyp2 j w b hb
Proof state after:
no goals
Theorem: clauseContains_prepend
Proof state before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
⊢ ∀ (kw : zero < succ n) (b : Bool), get' (v2 ::ᵥ cl2) zero kw = some b → get' (v1 ::ᵥ cl1) zero kw = some b
Tactic:
intro w b hb
Proof state after:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
w : zero < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) zero w = some b
⊢ get' (v1 ::ᵥ cl1) zero w = some b
Theorem: clauseContains_prepend
Proof state before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k : ℕ
w : zero < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) zero w = some b
⊢ get' (v1 ::ᵥ cl1) zero w = some b
Tactic:
exact hyp1 b hb
Proof state after:
no goals
Theorem: clauseContains_prepend
Proof state before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
⊢ ∀ (kw : j + 1 < succ n) (b : Bool), get' (v2 ::ᵥ cl2) (j + 1) kw = some b → get' (v1 ::ᵥ cl1) (j + 1) kw = some b
Tactic:
intro kw b hb
Proof state after:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ get' (v1 ::ᵥ cl1) (j + 1) kw = some b
Theorem: clauseContains_prepend
Proof state before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ get' (v1 ::ᵥ cl1) (j + 1) kw = some b
Tactic:
have w : j < n := by
    apply le_of_succ_le_succ
    exact kw
Proof state after:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
w : j < n
⊢ get' (v1 ::ᵥ cl1) (j + 1) kw = some b
Theorem: clauseContains_prepend
Proof state before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
w : j < n
⊢ get' (v1 ::ᵥ cl1) (j + 1) kw = some b
Tactic:
exact hyp2 j w b hb
Proof state after:
no goals
Theorem: clauseContains_prepend
Proof state before:
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ j < n
Tactic:
apply le_of_succ_le_succ
Proof state after:
case a
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ succ (succ j) ≤ succ n
Theorem: clauseContains_prepend
Proof state before:
case a
n : ℕ
v1 v2 : Option Bool
cl1 cl2 : Clause n
hyp1 : v1 ≥ v2
hyp2 : cl1⊇cl2
k j : ℕ
kw : j + 1 < succ n
b : Bool
hb : get' (v2 ::ᵥ cl2) (j + 1) kw = some b
⊢ succ (succ j) ≤ succ n
Tactic:
exact kw
Proof state after:
no goals
Theorem: clauseContains_implies_clauseContains_beyond
Proof state before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
⊢ cl1⊇cl2 → clauseContainsTail cl1 cl2 m
Tactic:
intro h k kw _ b
Proof state after:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : cl1⊇cl2
k : ℕ
kw : k < n
a✝ : m ≤ k
b : Bool
⊢ get' cl2 k kw = some b → get' cl1 k kw = some b
Theorem: clauseContains_implies_clauseContains_beyond
Proof state before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : cl1⊇cl2
k : ℕ
kw : k < n
a✝ : m ≤ k
b : Bool
⊢ get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
exact h k kw b
Proof state after:
no goals
Theorem: clauseContains_beyond_zero_implies_contains
Proof state before:
n : ℕ
cl1 cl2 : Clause n
⊢ clauseContainsTail cl1 cl2 zero → cl1⊇cl2
Tactic:
intro h k kw b
Proof state after:
n : ℕ
cl1 cl2 : Clause n
h : clauseContainsTail cl1 cl2 zero
k : ℕ
kw : k < n
b : Bool
⊢ get' cl2 k kw = some b → get' cl1 k kw = some b
Theorem: clauseContains_beyond_zero_implies_contains
Proof state before:
n : ℕ
cl1 cl2 : Clause n
h : clauseContainsTail cl1 cl2 zero
k : ℕ
kw : k < n
b : Bool
⊢ get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
exact h k kw (Nat.zero_le _) b
Proof state after:
no goals
Theorem: sat_of_contained_sat
Proof state before:
n : ℕ
cl1 cl2 : Clause n
⊢ cl1⊇cl2 → ∀ (valuation : Valuation n), ClauseSat cl2 valuation → ClauseSat cl1 valuation
Tactic:
intro num_clauses valuation
Proof state after:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
⊢ ClauseSat cl2 valuation → ClauseSat cl1 valuation
Theorem: sat_of_contained_sat
Proof state before:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
⊢ ClauseSat cl2 valuation → ClauseSat cl1 valuation
Tactic:
intro ⟨j, jw, vs⟩
Proof state after:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
⊢ ClauseSat cl1 valuation
Theorem: sat_of_contained_sat
Proof state before:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
⊢ ClauseSat cl1 valuation
Tactic:
let lem0 :  cl2.get' j jw = some (valuation.get' j jw) := vs
Proof state after:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
lem0 : get' cl2 j jw = some (get' valuation j jw) := vs
⊢ ClauseSat cl1 valuation
Theorem: sat_of_contained_sat
Proof state before:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
lem0 : get' cl2 j jw = some (get' valuation j jw) := vs
⊢ ClauseSat cl1 valuation
Tactic:
let lem1 : get' cl1 j jw = some (get' valuation j jw) := num_clauses j jw (valuation.get' j jw) lem0
Proof state after:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
lem0 : get' cl2 j jw = some (get' valuation j jw) := vs
lem1 : get' cl1 j jw = some (get' valuation j jw) := num_clauses j jw (get' valuation j jw) lem0
⊢ ClauseSat cl1 valuation
Theorem: sat_of_contained_sat
Proof state before:
n : ℕ
cl1 cl2 : Clause n
num_clauses : cl1⊇cl2
valuation : Valuation n
j : ℕ
jw : j < n
vs : VarSat (Vector.get cl2 { val := j, isLt := jw }) (Vector.get valuation { val := j, isLt := jw })
lem0 : get' cl2 j jw = some (get' valuation j jw) := vs
lem1 : get' cl1 j jw = some (get' valuation j jw) := num_clauses j jw (get' valuation j jw) lem0
⊢ ClauseSat cl1 valuation
Tactic:
exact ⟨j, jw, lem1⟩
Proof state after:
no goals
Theorem: clauseContains_beyond_vacuously
Proof state before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
⊢ n ≤ m → clauseContainsTail cl1 cl2 m
Tactic:
intro h k kw ineq
Proof state after:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Theorem: clauseContains_beyond_vacuously
Proof state before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
let inq := Nat.le_trans h ineq
Proof state after:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans h ineq
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Theorem: clauseContains_beyond_vacuously
Proof state before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans h ineq
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
let inq2 := Nat.lt_of_lt_of_le kw inq
Proof state after:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans h ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Theorem: clauseContains_beyond_vacuously
Proof state before:
n : ℕ
cl1 cl2 : Clause n
m : ℕ
h : n ≤ m
k : ℕ
kw : k < n
ineq : m ≤ k
inq : n ≤ k := Nat.le_trans h ineq
inq2 : k < k := Nat.lt_of_lt_of_le kw inq
⊢ ∀ (b : Bool), get' cl2 k kw = some b → get' cl1 k kw = some b
Tactic:
exact (False.elim (Nat.lt_irrefl k inq2))
Proof state after:
no goals
Theorem: get'_contradiction
Proof state before:
n k : ℕ
w : k < n
⊢ get' (contradiction n) k w = none
Tactic:
rw [contradiction, Vector.get'_of_Fn']
Proof state after:
no goals
Theorem: get_contradiction
Proof state before:
n : ℕ
kw : Fin n
⊢ Vector.get (contradiction n) kw = none
Tactic:
rw [contradiction, Vector.ofFn', Vector.get_ofFn]
Proof state after:
no goals
Theorem: contradiction_is_false
Proof state before:
n : ℕ
⊢ ∀ (valuation : Valuation n), ¬ClauseSat (contradiction n) valuation
Tactic:
intro valuation ⟨k, ⟨b, p⟩⟩
Proof state after:
n : ℕ
valuation : Valuation n
k : ℕ
b : k < n
p : VarSat (Vector.get (contradiction n) { val := k, isLt := b }) (Vector.get valuation { val := k, isLt := b })
⊢ False
Theorem: contradiction_is_false
Proof state before:
n : ℕ
valuation : Valuation n
k : ℕ
b : k < n
p : VarSat (Vector.get (contradiction n) { val := k, isLt := b }) (Vector.get valuation { val := k, isLt := b })
⊢ False
Tactic:
simp [get_contradiction, VarSat] at p
Proof state after:
no goals
Theorem: contradiction_insert_none
Proof state before:
n focus : ℕ
focusLt : focus < n + 1
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) = get' (contradiction (n + 1))
Tactic:
apply funext
Proof state after:
case h
n focus : ℕ
focusLt : focus < n + 1
⊢ ∀ (x : ℕ), FinSeq.insert none n focus focusLt (get' (contradiction n)) x = get' (contradiction (n + 1)) x
Theorem: contradiction_insert_none
Proof state before:
case h
n focus : ℕ
focusLt : focus < n + 1
⊢ ∀ (x : ℕ), FinSeq.insert none n focus focusLt (get' (contradiction n)) x = get' (contradiction (n + 1)) x
Tactic:
intro j
Proof state after:
case h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j = get' (contradiction (n + 1)) j
Theorem: contradiction_insert_none
Proof state before:
case h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j = get' (contradiction (n + 1)) j
Tactic:
apply funext
Proof state after:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
⊢ ∀ (x : j < succ n), FinSeq.insert none n focus focusLt (get' (contradiction n)) j x = get' (contradiction (n + 1)) j x
Theorem: contradiction_insert_none
Proof state before:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
⊢ ∀ (x : j < succ n), FinSeq.insert none n focus focusLt (get' (contradiction n)) j x = get' (contradiction (n + 1)) j x
Tactic:
intro jw
Proof state after:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = get' (contradiction (n + 1)) j jw
Theorem: contradiction_insert_none
Proof state before:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = get' (contradiction (n + 1)) j jw
Tactic:
rw [get'_contradiction]
Proof state after:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Theorem: contradiction_insert_none
Proof state before:
case h.h
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
exact if c : j = focus then
  match focus, c, focusLt with
  | .(j), rfl, .(jw) =>
    by
      rw [insert_at_focus]
else by
  let i := skipInverse focus j c
  let eqn : skip focus i = j := skipInverse_eq focus j c
  let iw := skip_preimage_lt focusLt jw eqn
  match j, eqn, jw with
  | .(skip focus i), rfl, .(skip_le_succ iw) =>
    rw [insert_at_image
        none n focus focusLt ((contradiction n).get')
        i iw, get'_contradiction]
Proof state after:
no goals
Theorem: contradiction_insert_none
Proof state before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : j = focus
⊢ FinSeq.insert none n j jw (get' (contradiction n)) j jw = none
Tactic:
rw [insert_at_focus]
Proof state after:
no goals
Theorem: contradiction_insert_none
Proof state before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
let i := skipInverse focus j c
Proof state after:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Theorem: contradiction_insert_none
Proof state before:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none
Tactic:
let eqn : skip focus i = j := skipInverse_eq focus j c
Proof state after:
n focus : ℕ
focusLt : focus < n + 1
j : ℕ
jw : j < succ n
c : ¬j = focus
i : ℕ := skipInverse focus j c
eqn : skip focus i = j := skipInverse_eq focus j c
⊢ FinSeq.insert none n focus focusLt (get' (contradiction n)) j jw = none