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

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ equivalent φ₁ φ₂ ↔ entails φ₁ φ₂ ∧ entails φ₂ φ₁
Tactic:
simp only [equivalent, entails]
State after:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ (∀ (τ : PropAssignment ν), eval τ φ₁ = eval τ φ₂) ↔
    (∀ (τ : PropAssignment ν), eval τ φ₁ ≤ eval τ φ₂) ∧ ∀ (τ : PropAssignment ν), eval τ φ₂ ≤ eval τ φ₁

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
φ φ₁ φ₂ φ₃ : PropForm ν
⊢ (∀ (τ : PropAssignment ν), eval τ φ₁ = eval τ φ₂) ↔
    (∀ (τ : PropAssignment ν), eval τ φ₁ ≤ eval τ φ₂) ∧ ∀ (τ : PropAssignment ν), eval τ φ₂ ≤ eval τ φ₁
Tactic:
aesop (add safe le_antisymm)
State after:
no goals