Theorem: LeanSAT.Encode.EncCNF.LawfulState.semVars_toPropFun_cnf_lt (LeanSAT/Encode/EncCNF.lean)

State before:
ν : Type u_1
s : LawfulState ν
⊢ ∀ v ∈ PropFun.semVars (Cnf.toPropFun s.cnf), v < s.nextVar
Tactic:
intro v h
State after:
ν : Type u_1
s : LawfulState ν
v : IVar
h : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ v < s.nextVar

State before:
ν : Type u_1
s : LawfulState ν
v : IVar
h : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ v < s.nextVar
Tactic:
replace h := Cnf.mem_semVars_toPropFun _ _ h
State after:
ν : Type u_1
s : LawfulState ν
v : IVar
h : ∃ C ∈ s.cnf, v ∈ PropFun.semVars (Clause.toPropFun C)
⊢ v < s.nextVar

State before:
ν : Type u_1
s : LawfulState ν
v : IVar
h : ∃ C ∈ s.cnf, v ∈ PropFun.semVars (Clause.toPropFun C)
⊢ v < s.nextVar
Tactic:
rcases h with ⟨C,hC,h⟩
State after:
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : v ∈ PropFun.semVars (Clause.toPropFun C)
⊢ v < s.nextVar

State before:
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : v ∈ PropFun.semVars (Clause.toPropFun C)
⊢ v < s.nextVar
Tactic:
replace h := Clause.mem_semVars_toPropFun _ _ h
State after:
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : ∃ l ∈ C, LitVar.toVar l = v
⊢ v < s.nextVar

State before:
case intro.intro
ν : Type u_1
s : LawfulState ν
v : IVar
C : Clause ILit
hC : C ∈ s.cnf
h : ∃ l ∈ C, LitVar.toVar l = v
⊢ v < s.nextVar
Tactic:
rcases h with ⟨l,hl,rfl⟩
State after:
case intro.intro.intro.intro
ν : Type u_1
s : LawfulState ν
C : Clause ILit
hC : C ∈ s.cnf
l : ILit
hl : l ∈ C
⊢ LitVar.toVar l < s.nextVar

State before:
case intro.intro.intro.intro
ν : Type u_1
s : LawfulState ν
C : Clause ILit
hC : C ∈ s.cnf
l : ILit
hl : l ∈ C
⊢ LitVar.toVar l < s.nextVar
Tactic:
apply s.cnfVarsLt _ hC _ hl
State after:
no goals