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

State before:
ν : Type u_1
s : LawfulState ν
n : ℕ
⊢ interp (withTemps s) = fun τ => interp s (PropAssignment.map Sum.inl τ)
Tactic:
ext τ
State after:
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ interp (withTemps s) τ ↔ interp s (PropAssignment.map Sum.inl τ)

State before:
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ interp (withTemps s) τ ↔ interp s (PropAssignment.map Sum.inl τ)
Tactic:
simp [interp, withTemps, State.withTemps]
State after:
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf

State before:
case h.a
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) ↔
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
constructor
State after:
case h.a.mp
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) →
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf

case h.a.mpr
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) →
    ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf

State before:
case h.a.mp
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf) →
    ∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
rintro ⟨σ,rfl,h⟩
State after:
case h.a.mp.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ_1,
    PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ_1 ∧
      σ_1 ⊨ Cnf.toPropFun s.cnf

State before:
case h.a.mp.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ_1,
    PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ_1 ∧
      σ_1 ⊨ Cnf.toPropFun s.cnf
Tactic:
use σ
State after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ ∧
    σ ⊨ Cnf.toPropFun s.cnf

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ ∧
    σ ⊨ Cnf.toPropFun s.cnf
Tactic:
simp [h]
State after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) = PropAssignment.map s.vMap σ
Tactic:
ext v
State after:
case h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
v : ν
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) v = PropAssignment.map s.vMap σ v

State before:
case h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h : σ ⊨ Cnf.toPropFun s.cnf
v : ν
⊢ PropAssignment.map Sum.inl (PropAssignment.map (State.withTemps.vMap s.toState) σ) v = PropAssignment.map s.vMap σ v
Tactic:
simp [State.withTemps.vMap]
State after:
no goals

State before:
case h.a.mpr
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
⊢ (∃ σ, PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ ∧ σ ⊨ Cnf.toPropFun s.cnf) →
    ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
rintro ⟨σ,h1,h2⟩
State after:
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf

State before:
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
have ⟨σ',hσ'⟩ := τ.exists_preimage ⟨State.withTemps.vMap s.toState, (LawfulState.withTemps s).vMapInj⟩
State after:
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
hσ' : τ = PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ'
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf

State before:
case h.a.mpr.intro.intro
ν : Type u_1
s : LawfulState ν
n : ℕ
τ : PropAssignment (ν ⊕ Fin n)
σ : PropAssignment IVar
h1 : PropAssignment.map Sum.inl τ = PropAssignment.map s.vMap σ
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
hσ' : τ = PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ'
⊢ ∃ σ, τ = PropAssignment.map (State.withTemps.vMap s.toState) σ ∧ σ ⊨ Cnf.toPropFun s.cnf
Tactic:
cases hσ'
State after:
case h.a.mpr.intro.intro.refl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ ∃ σ,
    PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ' =
        PropAssignment.map (State.withTemps.vMap s.toState) σ ∧
      σ ⊨ Cnf.toPropFun s.cnf

State before:
case h.a.mpr.intro.intro.refl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ ∃ σ,
    PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ' =
        PropAssignment.map (State.withTemps.vMap s.toState) σ ∧
      σ ⊨ Cnf.toPropFun s.cnf
Tactic:
simp [PropAssignment.map] at h2 ⊢
State after:
case h.a.mpr.intro.intro.refl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ ∃ σ, σ' ∘ State.withTemps.vMap s.toState = σ ∘ State.withTemps.vMap s.toState ∧ σ ⊨ Cnf.toPropFun s.cnf

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ σ' ∘ State.withTemps.vMap s.toState =
      PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState ∧
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ⊨
      Cnf.toPropFun s.cnf
Tactic:
constructor
State after:
case h.left
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ σ' ∘ State.withTemps.vMap s.toState =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
      State.withTemps.vMap s.toState

case h.right
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ⊨
    Cnf.toPropFun s.cnf

State before:
case h.left
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ σ' ∘ State.withTemps.vMap s.toState =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
      State.withTemps.vMap s.toState
Tactic:
ext vot
State after:
case h.left.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
vot : ν ⊕ Fin n
⊢ (σ' ∘ State.withTemps.vMap s.toState) vot =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      vot

State before:
case h.left.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
vot : ν ⊕ Fin n
⊢ (σ' ∘ State.withTemps.vMap s.toState) vot =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      vot
Tactic:
rcases vot with (v|t)
State after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)

case h.left.h.inr
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
t : Fin n
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inr t) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inr t)

State before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)
Tactic:
have := congrFun h1 v
State after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') v =
    PropAssignment.map s.vMap σ v
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)

State before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') v =
    PropAssignment.map s.vMap σ v
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)
Tactic:
simp at this
State after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this : σ' (State.withTemps.vMap s.toState (Sum.inl v)) = σ (s.vMap v)
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)

State before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this : σ' (State.withTemps.vMap s.toState (Sum.inl v)) = σ (s.vMap v)
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inl v) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inl v)
Tactic:
simp [this]
State after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this : σ' (State.withTemps.vMap s.toState (Sum.inl v)) = σ (s.vMap v)
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))

State before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
this : σ' (State.withTemps.vMap s.toState (Sum.inl v)) = σ (s.vMap v)
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))
Tactic:
clear this h2
State after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))

State before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ'
      (State.withTemps.vMap s.toState (Sum.inl v))
Tactic:
simp [withTemps, State.withTemps, State.withTemps.vMap]
State after:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ) σ'
      (s.vMap v)

State before:
case h.left.h.inl
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ σ (s.vMap v) =
    PropAssignment.setMany σ (Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ) σ'
      (s.vMap v)
Tactic:
rw [PropAssignment.setMany_not_mem]
State after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ s.vMap v ∉ Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ

State before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ s.vMap v ∉ Finset.image (fun x => { val := ↑s.nextVar + ↑x, property := ⋯ }) Finset.univ
Tactic:
simp
State after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ ∀ (x : Fin n), ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v

State before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
⊢ ∀ (x : Fin n), ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Tactic:
intro x
State after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
⊢ ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v

State before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
⊢ ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Tactic:
have := s.vMapLt v
State after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : s.vMap v < s.nextVar
⊢ ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v

State before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : s.vMap v < s.nextVar
⊢ ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = s.vMap v
Tactic:
rw [←Subtype.val_inj]
State after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : s.vMap v < s.nextVar
⊢ ¬↑{ val := ↑s.nextVar + ↑x, property := ⋯ } = ↑(s.vMap v)

State before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : s.vMap v < s.nextVar
⊢ ¬↑{ val := ↑s.nextVar + ↑x, property := ⋯ } = ↑(s.vMap v)
Tactic:
rw [← PNat.coe_lt_coe] at this
State after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ¬↑{ val := ↑s.nextVar + ↑x, property := ⋯ } = ↑(s.vMap v)

State before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ¬↑{ val := ↑s.nextVar + ↑x, property := ⋯ } = ↑(s.vMap v)
Tactic:
simp
State after:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ¬↑s.nextVar + ↑x = ↑(s.vMap v)

State before:
case h.left.h.inl.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ¬↑s.nextVar + ↑x = ↑(s.vMap v)
Tactic:
apply Nat.ne_of_gt
State after:
case h.left.h.inl.h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ↑(s.vMap v) < ↑s.nextVar + ↑x

State before:
case h.left.h.inl.h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : ν
x : Fin n
this : ↑(s.vMap v) < ↑s.nextVar
⊢ ↑(s.vMap v) < ↑s.nextVar + ↑x
Tactic:
exact Nat.lt_add_right _ this
State after:
no goals

State before:
case h.left.h.inr
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
t : Fin n
⊢ (σ' ∘ State.withTemps.vMap s.toState) (Sum.inr t) =
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ∘
        State.withTemps.vMap s.toState)
      (Sum.inr t)
Tactic:
simp [State.withTemps.vMap]
State after:
no goals

State before:
case h.right
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' ⊨
    Cnf.toPropFun s.cnf
Tactic:
apply (Model.PropFun.agreeOn_semVars _).mpr h2
State after:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.agreeOn (↑(PropFun.semVars (Cnf.toPropFun s.cnf)))
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ') σ

State before:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
⊢ PropAssignment.agreeOn (↑(PropFun.semVars (Cnf.toPropFun s.cnf)))
    (PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ') σ
Tactic:
intro v hv
State after:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ ↑(PropFun.semVars (Cnf.toPropFun s.cnf))
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v

State before:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ ↑(PropFun.semVars (Cnf.toPropFun s.cnf))
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Tactic:
simp at hv
State after:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v

State before:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Tactic:
have := semVars_toPropFun_cnf_lt _ _ hv
State after:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v

State before:
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ PropAssignment.setMany σ (Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ) σ' v = σ v
Tactic:
rw [PropAssignment.setMany_not_mem]
State after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ v ∉ Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ v ∉ Finset.image (fun x => State.withTemps.vMap s.toState (Sum.inr x)) Finset.univ
Tactic:
simp [State.withTemps.vMap]
State after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ ∀ (x : Fin n), ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = v

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
⊢ ∀ (x : Fin n), ¬{ val := ↑s.nextVar + ↑x, property := ⋯ } = v
Tactic:
intro v'
State after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
v' : Fin n
⊢ ¬{ val := ↑s.nextVar + ↑v', property := ⋯ } = v

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
v' : Fin n
⊢ ¬{ val := ↑s.nextVar + ↑v', property := ⋯ } = v
Tactic:
rw [←Subtype.val_inj]
State after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : v < s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v
Tactic:
rw [← PNat.coe_lt_coe] at this
State after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑{ val := ↑s.nextVar + ↑v', property := ⋯ } = ↑v
Tactic:
simp
State after:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑s.nextVar + ↑v' = ↑v

State before:
case h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ¬↑s.nextVar + ↑v' = ↑v
Tactic:
apply Nat.ne_of_gt
State after:
case h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ↑v < ↑s.nextVar + ↑v'

State before:
case h.h
ν : Type u_1
s : LawfulState ν
n : ℕ
σ : PropAssignment IVar
h2 : σ ⊨ Cnf.toPropFun s.cnf
σ' : PropAssignment IVar
h1 :
  PropAssignment.map Sum.inl (PropAssignment.map (⇑{ toFun := State.withTemps.vMap s.toState, inj' := ⋯ }) σ') =
    PropAssignment.map s.vMap σ
v : IVar
hv : v ∈ PropFun.semVars (Cnf.toPropFun s.cnf)
this : ↑v < ↑s.nextVar
v' : Fin n
⊢ ↑v < ↑s.nextVar + ↑v'
Tactic:
exact Nat.lt_add_right _ this
State after:
no goals