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

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
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 ψ

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 ⊢
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 ψ

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
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 ψ

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]
State after:
no goals

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
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 ψ

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
State after:
case var.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ : PropForm ν
v : ν
h✝ : ¬v = v✝
⊢ v = v ∧ ¬v = v✝ ∨ v ∈ vars ψ

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 [*]
State after:
no goals

State before:
case tr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ : PropForm ν
⊢ vars (substOne tr v ψ) ⊆ vars tr \ {v} ∪ vars ψ
Tactic:
simp
State after:
no goals

State before:
case fls
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁ φ₂ : PropForm ν
v : ν
ψ ψ₁ ψ₂ : PropForm ν
⊢ vars (substOne fls v ψ) ⊆ vars fls \ {v} ∪ vars ψ
Tactic:
simp
State after:
no goals

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
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 ψ

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
State after:
no goals

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
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 ψ

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 *
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 ψ

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
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 ψ

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₁ ‹_›
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 ψ

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')
this : v ∈ vars φ₁ \ {v✝} ∪ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
simp at this
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 = v✝ ∨ v ∈ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ

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')
this : v ∈ vars φ₁ ∧ ¬v = v✝ ∨ v ∈ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
rcases this with ⟨a,b⟩|c <;> simp [*]
State after:
no goals

State before:
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 ψ
Tactic:
have := ih₂ ‹_›
State after:
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')
this : v ∈ vars φ₂ \ {v✝} ∪ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ

State before:
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')
this : v ∈ vars φ₂ \ {v✝} ∪ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
simp at this
State after:
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')
this : v ∈ vars φ₂ ∧ ¬v = v✝ ∨ v ∈ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ

State before:
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')
this : v ∈ vars φ₂ ∧ ¬v = v✝ ∨ v ∈ vars ψ
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
Tactic:
rcases this with ⟨a,b⟩|c <;> simp [*]
State after:
no goals