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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
⊢ toPropFun (and f1 f2) = toPropFun f1 ⊓ toPropFun f2
Tactic:
ext τ
State after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (and f1 f2) ↔ τ ⊨ toPropFun f1 ⊓ toPropFun f2

State before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (and f1 f2) ↔ τ ⊨ toPropFun f1 ⊓ toPropFun f2
Tactic:
simp [satisfies_iff, Array.mem_def, and]
State after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ (∀ (C : Clause L), C ∈ f1.data ∨ C ∈ f2.data → τ ⊨ Clause.toPropFun C) ↔
    (∀ C ∈ f1.data, τ ⊨ Clause.toPropFun C) ∧ ∀ C ∈ f2.data, τ ⊨ Clause.toPropFun C

State before:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
f1 f2 : Cnf L
τ : PropAssignment ν
⊢ (∀ (C : Clause L), C ∈ f1.data ∨ C ∈ f2.data → τ ⊨ Clause.toPropFun C) ↔
    (∀ C ∈ f1.data, τ ⊨ Clause.toPropFun C) ∧ ∀ C ∈ f2.data, τ ⊨ Clause.toPropFun C
Tactic:
aesop
State after:
no goals