Theorem: LeanSAT.Model.PropFun.equivalentOver_semVars (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
⊢ ↑(semVars φ₁) ⊆ X → ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → φ₁ = φ₂
Tactic:
suffices ∀ {φ₁ φ₂} {τ : PropAssignment ν}, φ₂.semVars ⊆ X →
    equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂ by
  intro h₁ h₂ e
  ext τ
  exact ⟨this h₂ e, this h₁ e.symm⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
⊢ ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
⊢ ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
Tactic:
intro φ₁ φ₂ τ h₂ e h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
⊢ τ ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
⊢ τ ⊨ φ₂
Tactic:
have ⟨σ₁, hA, hS⟩ := (e τ).mp ⟨τ, τ.agreeOn_refl _, h⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
⊢ τ ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
⊢ τ ⊨ φ₂
Tactic:
have : σ₁ ⊨ φ₂ ↔ τ ⊨ φ₂ := agreeOn_semVars (hA.subset h₂)
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
this : σ₁ ⊨ φ₂ ↔ τ ⊨ φ₂
⊢ τ ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X : Set ν
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
h : τ ⊨ φ₁
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₂
this : σ₁ ⊨ φ₂ ↔ τ ⊨ φ₂
⊢ τ ⊨ φ₂
Tactic:
exact this.mp hS
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
⊢ ↑(semVars φ₁) ⊆ X → ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → φ₁ = φ₂
Tactic:
intro h₁ h₂ e
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
h₁ : ↑(semVars φ₁) ⊆ X
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
⊢ φ₁ = φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
h₁ : ↑(semVars φ₁) ⊆ X
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
⊢ φ₁ = φ₂
Tactic:
ext τ
State after:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
h₁ : ↑(semVars φ₁) ⊆ X
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ↔ τ ⊨ φ₂

State before:
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X : Set ν
this : ∀ {φ₁ φ₂ : PropFun ν} {τ : PropAssignment ν}, ↑(semVars φ₂) ⊆ X → equivalentOver X φ₁ φ₂ → τ ⊨ φ₁ → τ ⊨ φ₂
h₁ : ↑(semVars φ₁) ⊆ X
h₂ : ↑(semVars φ₂) ⊆ X
e : equivalentOver X φ₁ φ₂
τ : PropAssignment ν
⊢ τ ⊨ φ₁ ↔ τ ⊨ φ₂
Tactic:
exact ⟨this h₂ e, this h₁ e.symm⟩
State after:
no goals