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

State before:
ν : Type u_1
φ₁ φ₂ : PropFun ν
⊢ entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
have ⟨φ₁, h₁⟩ := Quotient.exists_rep φ₁
State after:
ν : Type u_1
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ entails φ₁✝ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂

State before:
ν : Type u_1
φ₁✝ φ₂ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
⊢ entails φ₁✝ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂
Tactic:
have ⟨φ₂, h₂⟩ := Quotient.exists_rep φ₂
State after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ entails φ₁✝ φ₂✝ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂✝

State before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ entails φ₁✝ φ₂✝ ↔ ∀ (τ : PropAssignment ν), τ ⊨ φ₁✝ → τ ⊨ φ₂✝
Tactic:
simp only [← h₁, ← h₂, entails_mk]
State after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ PropForm.entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ → τ ⊨ ⟦φ₂⟧

State before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
⊢ PropForm.entails φ₁ φ₂ ↔ ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ → τ ⊨ ⟦φ₂⟧
Tactic:
exact PropForm.entails_ext
State after:
no goals