Theorem: LeanSAT.Model.PropFun.tr_entails_disj_neg (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ tr ≤ eval τ (disj φ (neg φ))
Tactic:
simp only [eval_disj, eval_neg]
State after:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ tr ≤ (eval τ φ || !eval τ φ)

State before:
ν : Type u_1
φ : PropFun ν
τ : PropAssignment ν
⊢ eval τ tr ≤ (eval τ φ || !eval τ φ)
Tactic:
exact BooleanAlgebra.top_le_sup_compl (eval τ φ)
State after:
no goals