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