Theorem: LeanSAT.Model.PropFun.equivalentOver.subset (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
⊢ X ⊆ Y → equivalentOver Y φ₁ φ₂ → equivalentOver X φ₁ φ₂
Tactic:
intro hSub
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ equivalentOver Y φ₁ φ₂ → equivalentOver X φ₁ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ equivalentOver Y φ₁ φ₂ → equivalentOver X φ₁ φ₂
Tactic:
suffices ∀ φ₁ φ₂ τ, equivalentOver Y φ₁ φ₂ →
    (∃ (σ₁ : PropAssignment ν), σ₁.agreeOn X τ ∧ σ₁ ⊨ φ₁) →
    ∃ (σ₂ : PropAssignment ν), σ₂.agreeOn X τ ∧ σ₂ ⊨ φ₂ from
  fun e τ => ⟨this φ₁ φ₂ τ e, this φ₂ φ₁ τ e.symm⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ ∀ (φ₁ φ₂ : PropFun ν) (τ : PropAssignment ν),
    equivalentOver Y φ₁ φ₂ →
      (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
⊢ ∀ (φ₁ φ₂ : PropFun ν) (τ : PropAssignment ν),
    equivalentOver Y φ₁ φ₂ →
      (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
intro φ₁ φ₂ τ e ⟨σ₁, hA, hS⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
e : equivalentOver Y φ₁ φ₂
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂

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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ₁✝ φ₂✝ : PropFun ν
X Y : Set ν
hSub : X ⊆ Y
φ₁ φ₂ : PropFun ν
τ : PropAssignment ν
e : equivalentOver Y φ₁ φ₂
σ₁ : PropAssignment ν
hA : PropAssignment.agreeOn X σ₁ τ
hS : σ₁ ⊨ φ₁
σ₃ : PropAssignment ν
hA' : PropAssignment.agreeOn Y σ₃ σ₁
hS' : σ₃ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
exact ⟨σ₃, hA'.subset hSub |>.trans hA, hS'⟩
State after:
no goals