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

State before:
ν : Type u_1
φ₁ φ₂ φ₃ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ (conj (disj φ₁ φ₂) (disj φ₁ φ₃)) ≤ eval x✝ (disj φ₁ (conj φ₂ φ₃))
Tactic:
simp only [eval_conj, eval_disj]
State after:
ν : Type u_1
φ₁ φ₂ φ₃ : PropFun ν
x✝ : PropAssignment ν
⊢ ((eval x✝ φ₁ || eval x✝ φ₂) && (eval x✝ φ₁ || eval x✝ φ₃)) ≤ (eval x✝ φ₁ || eval x✝ φ₂ && eval x✝ φ₃)

State before:
ν : Type u_1
φ₁ φ₂ φ₃ : PropFun ν
x✝ : PropAssignment ν
⊢ ((eval x✝ φ₁ || eval x✝ φ₂) && (eval x✝ φ₁ || eval x✝ φ₃)) ≤ (eval x✝ φ₁ || eval x✝ φ₂ && eval x✝ φ₃)
Tactic:
exact le_sup_inf
State after:
no goals