internlm/Lean-Github huggingface dataset:
Theorem: LeanSAT.Model.PropForm.equivalent_ext
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ equivalent φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂
Tactic:
simp only [equivalent_iff_entails, entails_ext]
Proof state after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ ((∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂) ∧ ∀ (τ : PropAssignment ν), τ ⊨ φ₂ → τ ⊨ φ₁) ↔
    ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂
Theorem: LeanSAT.Model.PropForm.equivalent_ext
Proof state before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ ((∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂) ∧ ∀ (τ : PropAssignment ν), τ ⊨ φ₂ → τ ⊨ φ₁) ↔
    ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂
Tactic:
aesop
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.subst_assoc
Proof state before:
ν₁ : Type u_3
ν₂ : Type u_2
ν₃ : Type u_1
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
⊢ subst (subst φ f₁) f₂ = subst φ fun v => subst (f₁ v) f₂
Tactic:
induction φ <;> simp [subst, *]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.5697
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
inst✝¹ : DecidableEq ν₁
inst✝ : DecidableEq ν₂
⊢ vars (subst φ f) = Finset.biUnion (vars φ) fun v1 => vars (f v1)
Tactic:
induction φ <;> simp [subst, Finset.biUnion_union, *]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_subst
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.10308
f✝ f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ✝ φ₁ φ₂ φ : PropForm ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ subst φ f ↔ PropAssignment.subst (fun x => ⟦f x⟧) τ ⊨ φ
Tactic:
induction φ <;> simp [subst, PropAssignment.subst, *]
Proof state after:
case var
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.10308
f✝ f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
x✝ : ν₁
⊢ τ ⊨ f x✝ ↔ τ ⊨ ⟦f x✝⟧
Theorem: LeanSAT.Model.PropForm.satisfies_subst
Proof state before:
case var
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.10308
f✝ f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
x✝ : ν₁
⊢ τ ⊨ f x✝ ↔ τ ⊨ ⟦f x✝⟧
Tactic:
rw [PropFun.satisfies_mk]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.subst_congr
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
⊢ ∀ (σ : ν₁ → PropForm ν₂), ⟦subst φ₁ σ⟧ = ⟦subst φ₂ σ⟧
Tactic:
intro σ
Proof state after:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ⟦subst φ₁ σ⟧ = ⟦subst φ₂ σ⟧
Theorem: LeanSAT.Model.PropForm.subst_congr
Proof state before:
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ⟦subst φ₁ σ⟧ = ⟦subst φ₂ σ⟧
Tactic:
apply PropFun.ext
Proof state after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ∀ (τ : PropAssignment ν₂), τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Theorem: LeanSAT.Model.PropForm.subst_congr
Proof state before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
⊢ ∀ (τ : PropAssignment ν₂), τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Tactic:
intro τ
Proof state after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Theorem: LeanSAT.Model.PropForm.subst_congr
Proof state before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
σ : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Tactic:
rw [Quotient.eq] at hφ
Proof state after:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : φ₁ ≈ φ₂
σ : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Theorem: LeanSAT.Model.PropForm.subst_congr
Proof state before:
case a
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.14311
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁✝ φ₂✝ φ₁ φ₂ : PropForm ν₁
hφ : φ₁ ≈ φ₂
σ : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ ⟦subst φ₁ σ⟧ ↔ τ ⊨ ⟦subst φ₂ σ⟧
Tactic:
rw [PropFun.satisfies_mk, PropFun.satisfies_mk, satisfies_subst, satisfies_subst,
    ← PropFun.satisfies_mk, ← PropFun.satisfies_mk, Quotient.sound hφ]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.satisfies_substOne
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v : ν
τ : PropAssignment ν
⊢ τ ⊨ substOne φ v ψ ↔ PropAssignment.set τ v (decide (τ ⊨ ψ)) ⊨ φ
Tactic:
simp [substOne]
Proof 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 (τ ⊨ ψ)) ⊨ φ
Theorem: LeanSAT.Model.PropForm.satisfies_substOne
Proof 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
Proof 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 (τ ⊨ ψ)) ⊨ φ
Theorem: LeanSAT.Model.PropForm.satisfies_substOne
Proof 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
Proof 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 (τ ⊨ ψ))
Theorem: LeanSAT.Model.PropForm.satisfies_substOne
Proof 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
Proof 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
Theorem: LeanSAT.Model.PropForm.satisfies_substOne
Proof 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]
Proof 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
Theorem: LeanSAT.Model.PropForm.satisfies_substOne
Proof 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
Proof state after:
case a.e_a.h.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ✝ φ₁ φ₂ : PropForm ν
v✝¹ : ν
ψ ψ₁ ψ₂ φ : PropForm ν
v✝ : ν
τ : PropAssignment ν
v : ν
h✝ : v = v✝
⊢ τ ⊨ ⟦ψ⟧ ↔ τ ⊨ ψ
Theorem: LeanSAT.Model.PropForm.satisfies_substOne
Proof 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
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof state before:
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
⊢ ⟦substOne φ₁ v ψ₁⟧ = ⟦substOne φ₂ v ψ₂⟧
Tactic:
apply PropFun.ext
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
⊢ ∀ (τ : PropAssignment ν), τ ⊨ ⟦substOne φ₁ v ψ₁⟧ ↔ τ ⊨ ⟦substOne φ₂ v ψ₂⟧
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
⊢ ∀ (τ : PropAssignment ν), τ ⊨ ⟦substOne φ₁ v ψ₁⟧ ↔ τ ⊨ ⟦substOne φ₂ v ψ₂⟧
Tactic:
intro τ
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ τ ⊨ ⟦substOne φ₁ v ψ₁⟧ ↔ τ ⊨ ⟦substOne φ₂ v ψ₂⟧
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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]
Proof state after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ τ ⊨ substOne φ₁ v ψ₁ ↔ τ ⊨ substOne φ₂ v ψ₂
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof state before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁✝ ψ₂✝ φ₁ φ₂ ψ₁ ψ₂ : PropForm ν
v : ν
hφ : ⟦φ₁⟧ = ⟦φ₂⟧
hψ : ⟦ψ₁⟧ = ⟦ψ₂⟧
τ : PropAssignment ν
⊢ τ ⊨ substOne φ₁ v ψ₁ ↔ τ ⊨ substOne φ₂ v ψ₂
Tactic:
simp [substOne]
Proof 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⟧) τ ⊨ φ₂
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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φ]
Proof 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⟧) τ ⊨ ⟦φ₂⟧
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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
Proof 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⟧) τ ⊨ ⟦φ₂⟧
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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
Proof 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⟧) τ
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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
Proof 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
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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]
Proof 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⟧
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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
Proof 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⟧
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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ψ]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.substOne_congr
Proof 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
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case var
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ : ν
⊢ vars (substOne (var x✝) v ψ) ⊆ vars (var x✝) \ {v} ∪ vars ψ
Tactic:
intro v hv
Proof state after:
case var
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
hv : v ∈ vars (substOne (var x✝) v✝ ψ)
⊢ v ∈ vars (var x✝) \ {v✝} ∪ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case var
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
hv : v ∈ vars (substOne (var x✝) v✝ ψ)
⊢ v ∈ vars (var x✝) \ {v✝} ∪ vars ψ
Tactic:
simp [subst, substOne] at hv ⊢
Proof state after:
case var
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
hv : v ∈ vars (if x✝ = v✝ then ψ else var x✝)
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case var
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
hv : v ∈ vars (if x✝ = v✝ then ψ else var x✝)
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
split at hv
Proof state after:
case var.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
h✝ : x✝ = v✝
hv : v ∈ vars ψ
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ

case var.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
h✝ : ¬x✝ = v✝
hv : v ∈ vars (var x✝)
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case var.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
h✝ : x✝ = v✝
hv : v ∈ vars ψ
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
simp [hv]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case var.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
h✝ : ¬x✝ = v✝
hv : v ∈ vars (var x✝)
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
simp at hv
Proof state after:
case var.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
h✝ : ¬x✝ = v✝
hv : v = x✝
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case var.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
x✝ v : ν
h✝ : ¬x✝ = v✝
hv : v = x✝
⊢ v = x✝ ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
subst_vars
Proof state after:
case var.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
v : ν
h✝ : ¬v = v✝
⊢ v = v ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case var.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
v : ν
h✝ : ¬v = v✝
⊢ v = v ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
simp [*]
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case tr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ : PropForm ν
⊢ vars (substOne tr v ψ) ⊆ vars tr \ {v} ∪ vars ψ
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case fls
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ : PropForm ν
⊢ vars (substOne fls v ψ) ⊆ vars fls \ {v} ∪ vars ψ
Tactic:
simp
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case neg
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ φ₁ : PropForm ν
ih : vars (substOne φ₁ v ψ) ⊆ vars φ₁ \ {v} ∪ vars ψ
⊢ vars (substOne (neg φ₁) v ψ) ⊆ vars (neg φ₁) \ {v} ∪ vars ψ
Tactic:
simp
Proof state after:
case neg
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ φ₁ : PropForm ν
ih : vars (substOne φ₁ v ψ) ⊆ vars φ₁ \ {v} ∪ vars ψ
⊢ vars (subst φ₁ fun v' => if v' = v then ψ else var v') ⊆ vars φ₁ \ {v} ∪ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case neg
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ φ₁ : PropForm ν
ih : vars (substOne φ₁ v ψ) ⊆ vars φ₁ \ {v} ∪ vars ψ
⊢ vars (subst φ₁ fun v' => if v' = v then ψ else var v') ⊆ vars φ₁ \ {v} ∪ vars ψ
Tactic:
exact ih
Proof state after:
no goals
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v ψ) ⊆ vars φ₁ \ {v} ∪ vars ψ
ih₂ : vars (substOne φ₂ v ψ) ⊆ vars φ₂ \ {v} ∪ vars ψ
⊢ vars (substOne (biImpl φ₁ φ₂) v ψ) ⊆ vars (biImpl φ₁ φ₂) \ {v} ∪ vars ψ
Tactic:
intro v hv
Proof state after:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
hv : v ∈ vars (substOne (biImpl φ₁ φ₂) v✝ ψ)
⊢ v ∈ vars (biImpl φ₁ φ₂) \ {v✝} ∪ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
hv : v ∈ vars (substOne (biImpl φ₁ φ₂) v✝ ψ)
⊢ v ∈ vars (biImpl φ₁ φ₂) \ {v✝} ∪ vars ψ
Tactic:
simp at *
Proof state after:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
hv :
  v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v') ∨
    v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
hv :
  v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v') ∨
    v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
cases hv
Proof state after:
case biImpl.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ

case biImpl.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Theorem: LeanSAT.Model.PropForm.vars_substOne
Proof state before:
case biImpl.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
have := ih₁ ‹_›
Proof state after:
case biImpl.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v')
this : v ∈ vars φ₁ \ {v✝} ∪ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ