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

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

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