Theorem: LeanSAT.Model.PropFun.not_mem_semVars (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∉ semVars φ ↔ ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
simp [mem_semVars, -Bool.forall_bool]
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) ↔
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) ↔
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
constructor
State after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) →
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ) →
    ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ

State before:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ) →
    ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
intro h τ b
State after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ

State before:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
if b = τ x then
  simp_all
else
  have : b = !τ x := by apply Bool.eq_not_iff.mpr; assumption
  constructor <;> convert h _ ; simp [*]
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : b = τ x
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
simp_all
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
have : b = !τ x := by apply Bool.eq_not_iff.mpr; assumption
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
⊢ PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
Tactic:
constructor <;> convert h _
State after:
case h'.h.e'_4
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
a✝ : PropAssignment.set τ x b ⊨ φ
⊢ τ = PropAssignment.set (PropAssignment.set τ x b) x !PropAssignment.set τ x b x

State before:
case h'.h.e'_4
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
this : b = !τ x
a✝ : PropAssignment.set τ x b ⊨ φ
⊢ τ = PropAssignment.set (PropAssignment.set τ x b) x !PropAssignment.set τ x b x
Tactic:
simp [*]
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
⊢ b = !τ x
Tactic:
apply Bool.eq_not_iff.mpr
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
⊢ b ≠ τ x

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
τ : PropAssignment ν
b : Bool
h✝ : ¬b = τ x
⊢ b ≠ τ x
Tactic:
assumption
State after:
no goals

State before:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ (∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ) →
    ∀ (x_1 : PropAssignment ν), x_1 ⊨ φ → (PropAssignment.set x_1 x !x_1 x) ⊨ φ
Tactic:
intro h τ hτφ
State after:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ

State before:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
have := h τ (!τ x)
State after:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
this : (PropAssignment.set τ x !τ x) ⊨ φ ↔ τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ

State before:
case mpr
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
h : ∀ (τ : PropAssignment ν) (b : Bool), PropAssignment.set τ x b ⊨ φ ↔ τ ⊨ φ
τ : PropAssignment ν
hτφ : τ ⊨ φ
this : (PropAssignment.set τ x !τ x) ⊨ φ ↔ τ ⊨ φ
⊢ (PropAssignment.set τ x !τ x) ⊨ φ
Tactic:
simp [*]
State after:
no goals