Theorem: LeanSAT.Clause.toPropFun_map (LeanSAT/Data/Cnf.lean)

State before:
L : Type u
ν : Type v
inst✝² : LitVar L ν
L' : Type u_1
ν' : Type u_2
inst✝¹ : LitVar L' ν'
inst✝ : LawfulLitVar L' ν'
f : ν → ν'
c : Clause L
⊢ toPropFun (map L' f c) = PropFun.map f (toPropFun c)
Tactic:
ext τ
State after:
case a
L : Type u
ν : Type v
inst✝² : LitVar L ν
L' : Type u_1
ν' : Type u_2
inst✝¹ : LitVar L' ν'
inst✝ : LawfulLitVar L' ν'
f : ν → ν'
c : Clause L
τ : PropAssignment ν'
⊢ τ ⊨ toPropFun (map L' f c) ↔ τ ⊨ PropFun.map f (toPropFun c)

State before:
case a
L : Type u
ν : Type v
inst✝² : LitVar L ν
L' : Type u_1
ν' : Type u_2
inst✝¹ : LitVar L' ν'
inst✝ : LawfulLitVar L' ν'
f : ν → ν'
c : Clause L
τ : PropAssignment ν'
⊢ τ ⊨ toPropFun (map L' f c) ↔ τ ⊨ PropFun.map f (toPropFun c)
Tactic:
simp [map, satisfies_iff]
State after:
no goals