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

State before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
C : Clause L
⊢ τ ⊨ toPropFun C ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l
Tactic:
rw [toPropFun]
State after:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
C : Clause L
⊢ τ ⊨ any (Multiset.map LitVar.toPropFun ↑(Array.toList C)) ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l

State before:
L : Type u
ν : Type v
inst✝ : LitVar L ν
τ : PropAssignment ν
C : Clause L
⊢ τ ⊨ any (Multiset.map LitVar.toPropFun ↑(Array.toList C)) ↔ ∃ l ∈ C, τ ⊨ LitVar.toPropFun l
Tactic:
simp [Array.mem_def]
State after:
no goals