Theorem: LeanSAT.Model.PropForm.entails_ext (LeanSAT/Model/PropForm.lean)

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
have : ∀ τ, (φ₁.eval τ → φ₂.eval τ) ↔ φ₁.eval τ ≤ φ₂.eval τ := by
  intro τ
  cases (eval τ φ₁)
  . simp
  . simp only [true_implies]
    exact ⟨fun h => h ▸ le_rfl, top_unique⟩
State after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
this : ∀ (τ : PropAssignment ν), eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
this : ∀ (τ : PropAssignment ν), eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
simp [sEntails, entails, satisfies, this]
State after:
no goals

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ ∀ (τ : PropAssignment ν), eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
Tactic:
intro τ
State after:
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂

State before:
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₁ = true → eval τ φ₂ = true ↔ eval τ φ₁ ≤ eval τ φ₂
Tactic:
cases (eval τ φ₁)
State after:
case false
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ false = true → eval τ φ₂ = true ↔ false ≤ eval τ φ₂

case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂

State before:
case false
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ false = true → eval τ φ₂ = true ↔ false ≤ eval τ φ₂

case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Tactic:
. simp
State after:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂

State before:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Tactic:
. simp only [true_implies]
  exact ⟨fun h => h ▸ le_rfl, top_unique⟩
State after:
no goals

State before:
case false
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ false = true → eval τ φ₂ = true ↔ false ≤ eval τ φ₂
Tactic:
simp
State after:
no goals

State before:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ true = true → eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Tactic:
simp only [true_implies]
State after:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₂ = true ↔ true ≤ eval τ φ₂

State before:
case true
ν : Type u_1
τ✝ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
τ : PropAssignment ν
⊢ eval τ φ₂ = true ↔ true ≤ eval τ φ₂
Tactic:
exact ⟨fun h => h ▸ le_rfl, top_unique⟩
State after:
no goals