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

State before:
ν : Type u_1
F C : PropFun ν
⊢ F ≤ C → eqsat F (F ⊓ C)
Tactic:
intro h_entails
State after:
ν : Type u_1
F C : PropFun ν
h_entails : F ≤ C
⊢ eqsat F (F ⊓ C)

State before:
ν : Type u_1
F C : PropFun ν
h_entails : F ≤ C
⊢ eqsat F (F ⊓ C)
Tactic:
simp only [eqsat, satisfiable, ge_iff_le, satisfies_conj]
State after:
ν : Type u_1
F C : PropFun ν
h_entails : F ≤ C
⊢ (∃ τ, τ ⊨ F) ↔ ∃ τ, τ ⊨ F ∧ τ ⊨ C

State before:
ν : Type u_1
F C : PropFun ν
h_entails : F ≤ C
⊢ (∃ τ, τ ⊨ F) ↔ ∃ τ, τ ⊨ F ∧ τ ⊨ C
Tactic:
exact ⟨fun ⟨τ, hτ⟩ => ⟨τ, hτ, h_entails τ hτ⟩, fun ⟨τ, hτ, _⟩ => ⟨τ, hτ⟩⟩
State after:
no goals