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

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

State before:
ν✝ : Type u_1
φ₁ φ₃ φ₂ : PropFun ν✝
h₁ : entails φ₁ φ₃
h₂ : entails φ₂ φ₃
τ : PropAssignment ν✝
⊢ (eval τ φ₁ || eval τ φ₂) ≤ eval τ φ₃
Tactic:
exact sup_le (h₁ τ) (h₂ τ)
State after:
no goals