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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ ψ : PropFun ν
v : ν
τ : PropAssignment ν
⊢ τ ⊨ substOne ψ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ
Tactic:
have ⟨ψ,hψ⟩ := ψ.exists_rep
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ ψ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ : PropForm ν
hψ : ⟦ψ⟧ = ψ✝
⊢ τ ⊨ substOne ψ✝ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ✝

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ ψ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ : PropForm ν
hψ : ⟦ψ⟧ = ψ✝
⊢ τ ⊨ substOne ψ✝ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ✝
Tactic:
cases hψ
State after:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
v : ν
τ : PropAssignment ν
ψ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ⟦ψ⟧

State before:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
v : ν
τ : PropAssignment ν
ψ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ⟦ψ⟧
Tactic:
have ⟨φ,hφ⟩ := φ.exists_rep
State after:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
hφ : ⟦φ⟧ = φ✝
⊢ τ ⊨ substOne ⟦ψ⟧ v φ✝ ↔ PropAssignment.set τ v (decide (τ ⊨ φ✝)) ⊨ ⟦ψ⟧

State before:
case refl
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ : PropFun ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
hφ : ⟦φ⟧ = φ✝
⊢ τ ⊨ substOne ⟦ψ⟧ v φ✝ ↔ PropAssignment.set τ v (decide (τ ⊨ φ✝)) ⊨ ⟦ψ⟧
Tactic:
cases hφ
State after:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v ⟦φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧

State before:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ substOne ⟦ψ⟧ v ⟦φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧
Tactic:
simp [substOne]
State after:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ ⟦PropForm.substOne ψ v φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧

State before:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ ⟦PropForm.substOne ψ v φ⟧ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ⟦ψ⟧
Tactic:
rw [satisfies_mk, satisfies_mk]
State after:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ PropForm.substOne ψ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ

State before:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ τ ⊨ PropForm.substOne ψ v φ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ
Tactic:
rw [PropForm.satisfies_substOne]
State after:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ

State before:
case refl.refl
ν : Type u_1
inst✝ : DecidableEq ν
v : ν
τ : PropAssignment ν
ψ φ : PropForm ν
⊢ PropAssignment.set τ v (decide (τ ⊨ φ)) ⊨ ψ ↔ PropAssignment.set τ v (decide (τ ⊨ ⟦φ⟧)) ⊨ ψ
Tactic:
rfl
State after:
no goals