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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : Cnf L
⊢ τ ⊨ toPropFun φ ↔ ∀ C ∈ φ, τ ⊨ Clause.toPropFun C
Tactic:
rw [toPropFun]
State after:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : Cnf L
⊢ τ ⊨ all ↑(List.map Clause.toPropFun φ.data) ↔ ∀ C ∈ φ, τ ⊨ Clause.toPropFun C

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : Cnf L
⊢ τ ⊨ all ↑(List.map Clause.toPropFun φ.data) ↔ ∀ C ∈ φ, τ ⊨ Clause.toPropFun C
Tactic:
rcases φ with ⟨φ⟩
State after:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : List (Clause L)
⊢ τ ⊨ all ↑(List.map Clause.toPropFun { data := φ }.data) ↔ ∀ C ∈ { data := φ }, τ ⊨ Clause.toPropFun C

State before:
case mk
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
τ : PropAssignment ν
φ : List (Clause L)
⊢ τ ⊨ all ↑(List.map Clause.toPropFun { data := φ }.data) ↔ ∀ C ∈ { data := φ }, τ ⊨ Clause.toPropFun C
Tactic:
induction φ <;> simp_all [Array.mem_def]
State after:
no goals