Theorem: LeanSAT.Model.PropForm.satisfies_substOne (LeanSAT/Model/Subst.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ τ ⊨ substOne φ v ψ ↔ PropAssignment.set τ v (decide (τ ⊨ ψ)) ⊨ φ
Tactic:
simp [substOne]
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ else var x⟧) τ ⊨ φ ↔ PropAssignment.set τ v (decide (τ ⊨ ψ)) ⊨ φ

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ else var x⟧) τ ⊨ φ ↔ PropAssignment.set τ v (decide (τ ⊨ ψ)) ⊨ φ
Tactic:
apply iff_of_eq
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ else var x⟧) τ ⊨ φ = PropAssignment.set τ v (decide (τ ⊨ ψ)) ⊨ φ

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ else var x⟧) τ ⊨ φ = PropAssignment.set τ v (decide (τ ⊨ ψ)) ⊨ φ
Tactic:
congr
State after:
case a.e_a
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ else var x⟧) τ = PropAssignment.set τ v (decide (τ ⊨ ψ))

State before:
case a.e_a
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ PropAssignment.subst (fun x => ⟦if x = v then ψ else var x⟧) τ = PropAssignment.set τ v (decide (τ ⊨ ψ))
Tactic:
ext v
State after:
case a.e_a.h
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝¹ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v✝ : ν
τ : PropAssignment ν
v : ν
⊢ PropAssignment.subst (fun x => ⟦if x = v✝ then ψ else var x⟧) τ v = PropAssignment.set τ v✝ (decide (τ ⊨ ψ)) v

State before:
case a.e_a.h
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝¹ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v✝ : ν
τ : PropAssignment ν
v : ν
⊢ PropAssignment.subst (fun x => ⟦if x = v✝ then ψ else var x⟧) τ v = PropAssignment.set τ v✝ (decide (τ ⊨ ψ)) v
Tactic:
simp [PropAssignment.subst, PropAssignment.set]
State after:
case a.e_a.h
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝¹ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v✝ : ν
τ : PropAssignment ν
v : ν
⊢ decide (τ ⊨ ⟦if v = v✝ then ψ else var v⟧) = if v = v✝ then decide (τ ⊨ ψ) else τ v

State before:
case a.e_a.h
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝¹ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v✝ : ν
τ : PropAssignment ν
v : ν
⊢ decide (τ ⊨ ⟦if v = v✝ then ψ else var v⟧) = if v = v✝ then decide (τ ⊨ ψ) else τ v
Tactic:
split <;> simp
State after:
case a.e_a.h.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝¹ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v✝ : ν
τ : PropAssignment ν
v : ν
h✝ : v = v✝
⊢ τ ⊨ ⟦ψ⟧ ↔ τ ⊨ ψ

State before:
case a.e_a.h.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝¹ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v✝ : ν
τ : PropAssignment ν
v : ν
h✝ : v = v✝
⊢ τ ⊨ ⟦ψ⟧ ↔ τ ⊨ ψ
Tactic:
exact PropFun.satisfies_mk
State after:
no goals