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

State before:
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
C : Clause L
f : Cnf L
⊢ toPropFun (addClause C f) = toPropFun f ⊓ Clause.toPropFun C
Tactic:
ext τ
State after:
case a
L : Type u
ν : Type v
inst✝¹ : LitVar L ν
inst✝ : DecidableEq ν
C : Clause L
f : Cnf L
τ : PropAssignment ν
⊢ τ ⊨ toPropFun (addClause C f) ↔ τ ⊨ toPropFun f ⊓ Clause.toPropFun C

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

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