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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
⊢ ⟦substOne φ₁ v ψ₁⟧ = ⟦substOne φ₂ v ψ₂⟧
Tactic:
apply PropFun.ext
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
⊢ ∀ (τ : PropAssignment ν), τ ⊨ ⟦substOne φ₁ v ψ₁⟧ ↔ τ ⊨ ⟦substOne φ₂ v ψ₂⟧

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
⊢ ∀ (τ : PropAssignment ν), τ ⊨ ⟦substOne φ₁ v ψ₁⟧ ↔ τ ⊨ ⟦substOne φ₂ v ψ₂⟧
Tactic:
intro τ
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ τ ⊨ ⟦substOne φ₁ v ψ₁⟧ ↔ τ ⊨ ⟦substOne φ₂ v ψ₂⟧

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ τ ⊨ ⟦substOne φ₁ v ψ₁⟧ ↔ τ ⊨ ⟦substOne φ₂ v ψ₂⟧
Tactic:
rw [PropFun.satisfies_mk, PropFun.satisfies_mk]
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ τ ⊨ substOne φ₁ v ψ₁ ↔ τ ⊨ substOne φ₂ v ψ₂

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

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

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

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

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

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

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

case a.a.e_a.h.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝¹ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v✝ : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
v : ν
h✝ : ¬v = v✝
⊢ τ ⊨ ⟦var v⟧ ↔ τ ⊨ ⟦var v⟧

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

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