Theorem: LeanSAT.LitVar.satisfies_map (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ τ ⊨ toPropFun (map f l) ↔ PropAssignment.map f τ ⊨ toPropFun l
Tactic:
simp [map, toPropFun]
State after:
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ (τ ⊨ if polarity l = true then var (f (toVar l)) else (var (f (toVar l)))ᶜ) ↔
    PropAssignment.map f τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ

State before:
L : Type u
ν : Type v
inst✝⁵ : LitVar L ν
inst✝⁴ : LawfulLitVar L ν
inst✝³ : DecidableEq ν
V : Type u_1
L' : Type u_2
V' : Type u_3
inst✝² : LitVar L V
inst✝¹ : LitVar L' V'
inst✝ : LawfulLitVar L' V'
f : V → V'
l : L
τ : PropAssignment V'
⊢ (τ ⊨ if polarity l = true then var (f (toVar l)) else (var (f (toVar l)))ᶜ) ↔
    PropAssignment.map f τ ⊨ if polarity l = true then var (toVar l) else (var (toVar l))ᶜ
Tactic:
split <;> simp
State after:
no goals