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

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

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

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

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

State before:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
h : ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧
⊢ ⟦φ₁⟧ = ⟦φ₂⟧
Tactic:
apply Quotient.sound ∘ PropForm.equivalent_ext.mpr
State after:
ν : Type u_1
φ₁✝ φ₂✝ : PropFun ν
φ₁ : PropForm ν
h₁ : ⟦φ₁⟧ = φ₁✝
φ₂ : PropForm ν
h₂ : ⟦φ₂⟧ = φ₂✝
h : ∀ (τ : PropAssignment ν), τ ⊨ ⟦φ₁⟧ ↔ τ ⊨ ⟦φ₂⟧
⊢ ∀ (τ : PropAssignment ν), τ ⊨ φ₁ ↔ τ ⊨ φ₂

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