Theorem: LeanSAT.Model.PropFun.entails_disj_right (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_right
State after:
no goals