Theorem: LeanSAT.LitVar.toPropFun_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
⊢ toPropFun (map f l) = PropFun.map f (toPropFun l)
Tactic:
ext τ
State after:
case a
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) ↔ τ ⊨ PropFun.map f (toPropFun l)

State before:
case a
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) ↔ τ ⊨ PropFun.map f (toPropFun l)
Tactic:
simp
State after:
no goals