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

State before:
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
⊢ evalPrimeFfToNot (Function.updateITE V U b) '' Δ = evalPrimeFfToNot V '' Δ
Tactic:
apply Set.image_congr
State after:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
⊢ ∀ a ∈ Δ, evalPrimeFfToNot (Function.updateITE V U b) a = evalPrimeFfToNot V a

State before:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
⊢ ∀ a ∈ Δ, evalPrimeFfToNot (Function.updateITE V U b) a = evalPrimeFfToNot V a
Tactic:
intro U' a1
State after:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
⊢ evalPrimeFfToNot (Function.updateITE V U b) U' = evalPrimeFfToNot V U'

State before:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_Δ : ∀ U' ∈ Δ, U'.IsPrime
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
⊢ evalPrimeFfToNot (Function.updateITE V U b) U' = evalPrimeFfToNot V U'
Tactic:
specialize h1_Δ U' a1
State after:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U b) U' = evalPrimeFfToNot V U'

State before:
case h
U : Formula
Δ : Set Formula
V : VarBoolAssignment
b : Bool
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U b) U' = evalPrimeFfToNot V U'
Tactic:
cases b
State after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U false) U' = evalPrimeFfToNot V U'

case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U true) U' = evalPrimeFfToNot V U'

State before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U false) U' = evalPrimeFfToNot V U'
Tactic:
simp only [evalPrimeFfToNot_of_function_updateIte_false U' U V h1_Δ]
State after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U'.not_ U' = evalPrimeFfToNot V U'

State before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U'.not_ U' = evalPrimeFfToNot V U'
Tactic:
simp only [Function.updateITE]
State after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ (if U' = U then U'.not_ else evalPrimeFfToNot V U') = evalPrimeFfToNot V U'

State before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ (if U' = U then U'.not_ else evalPrimeFfToNot V U') = evalPrimeFfToNot V U'
Tactic:
simp
State after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ U' = U → U'.not_ = evalPrimeFfToNot V U'

State before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ U' = U → U'.not_ = evalPrimeFfToNot V U'
Tactic:
intro a2
State after:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U'.not_ = evalPrimeFfToNot V U'

State before:
case h.false
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U'.not_ = evalPrimeFfToNot V U'
Tactic:
subst a2
State after:
case h.false
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U'.not_ = evalPrimeFfToNot V U'

State before:
case h.false
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U'.not_ = evalPrimeFfToNot V U'
Tactic:
contradiction
State after:
no goals

State before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ evalPrimeFfToNot (Function.updateITE V U true) U' = evalPrimeFfToNot V U'
Tactic:
simp only [evalPrimeFfToNot_of_function_updateIte_true U' U V h1_Δ]
State after:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U' U' = evalPrimeFfToNot V U'

State before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ Function.updateITE (evalPrimeFfToNot V) U U' U' = evalPrimeFfToNot V U'
Tactic:
simp only [Function.updateITE]
State after:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ (if U' = U then U' else evalPrimeFfToNot V U') = evalPrimeFfToNot V U'

State before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ (if U' = U then U' else evalPrimeFfToNot V U') = evalPrimeFfToNot V U'
Tactic:
simp
State after:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ U' = U → U' = evalPrimeFfToNot V U'

State before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
⊢ U' = U → U' = evalPrimeFfToNot V U'
Tactic:
intro a2
State after:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U' = evalPrimeFfToNot V U'

State before:
case h.true
U : Formula
Δ : Set Formula
V : VarBoolAssignment
h1_U : U.IsPrime
h2 : U ∉ Δ
U' : Formula
a1 : U' ∈ Δ
h1_Δ : U'.IsPrime
a2 : U' = U
⊢ U' = evalPrimeFfToNot V U'
Tactic:
subst a2
State after:
case h.true
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U' = evalPrimeFfToNot V U'

State before:
case h.true
Δ : Set Formula
V : VarBoolAssignment
U' : Formula
a1 : U' ∈ Δ
h1_Δ h1_U : U'.IsPrime
h2 : U' ∉ Δ
⊢ U' = evalPrimeFfToNot V U'
Tactic:
contradiction
State after:
no goals