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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ ↔ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Tactic:
constructor
State after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ → extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁ → equivalentOver X φ₁ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ → extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Tactic:
case mp =>
  intro h
  exact ⟨fun σ₁ h₁ => h σ₁ |>.mp ⟨σ₁, σ₁.agreeOn_refl X, h₁⟩,
    fun σ₂ h₂ => h σ₂ |>.mpr ⟨σ₂, σ₂.agreeOn_refl X, h₂⟩⟩
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁ → equivalentOver X φ₁ φ₂
Tactic:
case mpr =>
  intro ⟨h₁, h₂⟩
  intro τ
  constructor
  case mp =>
    intro ⟨σ₁, hAgree₁, hσ₁⟩
    have ⟨σ₂, hAgree₂, hσ₂⟩ := h₁ σ₁ hσ₁
    exact ⟨σ₂, hAgree₂.trans hAgree₁, hσ₂⟩
  case mpr =>
    intro ⟨σ₂, hAgree₂, hσ₂⟩
    have ⟨σ₁, hAgree₁, hσ₁⟩ := h₂ σ₂ hσ₂
    exact ⟨σ₁, hAgree₁.trans hAgree₂, hσ₁⟩
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ equivalentOver X φ₁ φ₂ → extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Tactic:
intro h
State after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h : equivalentOver X φ₁ φ₂
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h : equivalentOver X φ₁ φ₂
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁
Tactic:
exact ⟨fun σ₁ h₁ => h σ₁ |>.mp ⟨σ₁, σ₁.agreeOn_refl X, h₁⟩,
  fun σ₂ h₂ => h σ₂ |>.mpr ⟨σ₂, σ₂.agreeOn_refl X, h₂⟩⟩
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
⊢ extendsOver X φ₁ φ₂ ∧ extendsOver X φ₂ φ₁ → equivalentOver X φ₁ φ₂
Tactic:
intro ⟨h₁, h₂⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
⊢ equivalentOver X φ₁ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
⊢ equivalentOver X φ₁ φ₂
Tactic:
intro τ
State after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) ↔ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) ↔ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
constructor
State after:
case mp
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂

case mpr
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂) → ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
case mp =>
  intro ⟨σ₁, hAgree₁, hσ₁⟩
  have ⟨σ₂, hAgree₂, hσ₂⟩ := h₁ σ₁ hσ₁
  exact ⟨σ₂, hAgree₂.trans hAgree₁, hσ₂⟩
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂) → ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Tactic:
case mpr =>
  intro ⟨σ₂, hAgree₂, hσ₂⟩
  have ⟨σ₁, hAgree₁, hσ₁⟩ := h₂ σ₂ hσ₂
  exact ⟨σ₁, hAgree₁.trans hAgree₂, hσ₁⟩
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁) → ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
intro ⟨σ₁, hAgree₁, hσ₁⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
have ⟨σ₂, hAgree₂, hσ₂⟩ := h₁ σ₁ hσ₁
State after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ σ₁
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ τ
hσ₁ : σ₁ ⊨ φ₁
σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ σ₁
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂
Tactic:
exact ⟨σ₂, hAgree₂.trans hAgree₁, hσ₂⟩
State after:
no goals

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ : PropAssignment ν
⊢ (∃ σ₂, PropAssignment.agreeOn X σ₂ τ ∧ σ₂ ⊨ φ₂) → ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Tactic:
intro ⟨σ₂, hAgree₂, hσ₂⟩
State after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ τ
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ τ
hσ₂ : σ₂ ⊨ φ₂
⊢ ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Tactic:
have ⟨σ₁, hAgree₁, hσ₁⟩ := h₂ σ₂ hσ₂
State after:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ τ
hσ₂ : σ₂ ⊨ φ₂
σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ σ₂
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁

State before:
ν : Type u_1
inst✝ : DecidableEq ν
X : Set ν
φ₁ φ₂ : PropFun ν
h₁ : extendsOver X φ₁ φ₂
h₂ : extendsOver X φ₂ φ₁
τ σ₂ : PropAssignment ν
hAgree₂ : PropAssignment.agreeOn X σ₂ τ
hσ₂ : σ₂ ⊨ φ₂
σ₁ : PropAssignment ν
hAgree₁ : PropAssignment.agreeOn X σ₁ σ₂
hσ₁ : σ₁ ⊨ φ₁
⊢ ∃ σ₁, PropAssignment.agreeOn X σ₁ τ ∧ σ₁ ⊨ φ₁
Tactic:
exact ⟨σ₁, hAgree₁.trans hAgree₂, hσ₁⟩
State after:
no goals