Theorem: FOL.NV.propCompleteAux (FOL/NV/Margaris/Prop.lean)

State before:
P : Formula
Δ_U : Finset Formula
h1 : Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
⊢ IsDeduct ∅ P
Tactic:
induction Δ_U using Finset.induction_on
State after:
case empty
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) ∅)) P
⊢ IsDeduct ∅ P

case insert
P a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : s✝ ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) s✝)) P) → IsDeduct ∅ P
h1 : insert a✝² s✝ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert a✝² s✝))) P
⊢ IsDeduct ∅ P

State before:
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) ∅)) P
⊢ IsDeduct ∅ P
Tactic:
case empty =>
  simp at h2
  exact h2
State after:
no goals

State before:
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) ∅)) P
⊢ IsDeduct ∅ P
Tactic:
simp at h2
State after:
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : IsDeduct ∅ P
⊢ IsDeduct ∅ P

State before:
P : Formula
h1 : ∅ ⊆ P.primeSet
h2 : IsDeduct ∅ P
⊢ IsDeduct ∅ P
Tactic:
exact h2
State after:
no goals

State before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ IsDeduct ∅ P
Tactic:
apply Δ_U_2
State after:
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ Δ_U ⊆ P.primeSet

case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P

State before:
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ Δ_U ⊆ P.primeSet
Tactic:
simp only [Finset.insert_subset_iff] at h1
State after:
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet

State before:
case h1
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet
Tactic:
cases h1
State after:
case h1.intro
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
left✝ : U ∈ P.primeSet
right✝ : Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet

State before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet
Tactic:
case intro h1_left h1_right =>
  exact h1_right
State after:
no goals

State before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ Δ_U ⊆ P.primeSet
Tactic:
exact h1_right
State after:
no goals

State before:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : insert U Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Tactic:
simp only [Finset.insert_subset_iff] at h1
State after:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P

State before:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) (insert U Δ_U))) P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Tactic:
simp at h2
State after:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P

State before:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h1 : U ∈ P.primeSet ∧ Δ_U ⊆ P.primeSet
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Tactic:
cases h1
State after:
case h2.intro
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
left✝ : U ∈ P.primeSet
right✝ : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P

State before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P
Tactic:
simp
State after:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U) P

State before:
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U) P
Tactic:
apply propCompleteAuxAux P U Δ_U
State after:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ U' ∈ ↑Δ_U, U'.IsPrime

case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U.IsPrime

case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∉ ↑Δ_U

case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U ∪ {evalPrimeFfToNot V U}) P

State before:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ U' ∈ ↑Δ_U, U'.IsPrime
Tactic:
intro U' a1
State after:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U'.IsPrime

State before:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U'.IsPrime
Tactic:
apply mem_primeSet_isPrime P U'
State after:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U' ∈ P.primeSet

State before:
case h1_Δ
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U' ∈ P.primeSet
Tactic:
apply h1_right
State after:
case h1_Δ.a
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U' ∈ Δ_U

State before:
case h1_Δ.a
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
U' : Formula
a1 : U' ∈ ↑Δ_U
⊢ U' ∈ Δ_U
Tactic:
exact a1
State after:
no goals

State before:
case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U.IsPrime
Tactic:
apply mem_primeSet_isPrime P U
State after:
case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∈ P.primeSet

State before:
case h1_U
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∈ P.primeSet
Tactic:
exact h1_left
State after:
no goals

State before:
case h2
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ U ∉ ↑Δ_U
Tactic:
exact Δ_U_1
State after:
no goals

State before:
case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (evalPrimeFfToNot V '' ↑Δ_U ∪ {evalPrimeFfToNot V U}) P
Tactic:
simp
State after:
case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P

State before:
case h3
P U : Formula
Δ_U : Finset Formula
Δ_U_1 : U ∉ Δ_U
Δ_U_2 :
  Δ_U ⊆ P.primeSet → (∀ (V : VarBoolAssignment), IsDeduct (↑(Finset.image (evalPrimeFfToNot V) Δ_U)) P) → IsDeduct ∅ P
h2 : ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
h1_left : U ∈ P.primeSet
h1_right : Δ_U ⊆ P.primeSet
⊢ ∀ (V : VarBoolAssignment), IsDeduct (insert (evalPrimeFfToNot V U) (evalPrimeFfToNot V '' ↑Δ_U)) P
Tactic:
exact h2
State after:
no goals