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

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
x✝ : PropAssignment ν
⊢ eval x✝ (conj φ₁ φ₂) ≤ eval x✝ φ₂
Tactic:
simp only [eval_conj]
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 inf_le_right
State after:
no goals