Theorem: LeanSAT.Model.PropFun.existsInv_existsInv (LeanSAT/Model/Quantifiers.lean)

State before:
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
⊢ existsInv f (existsInv g φ) = existsInv (g ∘ f) φ
Tactic:
ext τ
State after:
case a
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ τ ⊨ existsInv f (existsInv g φ) ↔ τ ⊨ existsInv (g ∘ f) φ

State before:
case a
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ τ ⊨ existsInv f (existsInv g φ) ↔ τ ⊨ existsInv (g ∘ f) φ
Tactic:
simp
State after:
case a
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) ↔
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ

State before:
case a
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) ↔
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ
Tactic:
constructor
State after:
case a.mp
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) →
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ

case a.mpr
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ) →
    ∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ

State before:
case a.mp
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ) →
    ∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ
Tactic:
rintro ⟨_, ⟨σ,h,rfl⟩, rfl⟩
State after:
case a.mp.intro.intro.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ_1

State before:
case a.mp.intro.intro.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ_1
Tactic:
use σ
State after:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ σ ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ

State before:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ σ ⊨ φ ∧ PropAssignment.map f (PropAssignment.map g σ) = PropAssignment.map (g ∘ f) σ
Tactic:
simp [*, PropAssignment.map]
State after:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (σ ∘ g) ∘ f = σ ∘ g ∘ f

State before:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (σ ∘ g) ∘ f = σ ∘ g ∘ f
Tactic:
rfl
State after:
no goals

State before:
case a.mpr
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
τ : PropAssignment ν''
⊢ (∃ σ, σ ⊨ φ ∧ τ = PropAssignment.map (g ∘ f) σ) →
    ∃ σ, (∃ σ_1, σ_1 ⊨ φ ∧ σ = PropAssignment.map g σ_1) ∧ τ = PropAssignment.map f σ
Tactic:
rintro ⟨σ,h,rfl⟩
State after:
case a.mpr.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, (∃ σ, σ ⊨ φ ∧ σ_1 = PropAssignment.map g σ) ∧ PropAssignment.map (g ∘ f) σ = PropAssignment.map f σ_1

State before:
case a.mpr.intro.intro
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, (∃ σ, σ ⊨ φ ∧ σ_1 = PropAssignment.map g σ) ∧ PropAssignment.map (g ∘ f) σ = PropAssignment.map f σ_1
Tactic:
use σ.map g
State after:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map g σ = PropAssignment.map g σ_1) ∧
    PropAssignment.map (g ∘ f) σ = PropAssignment.map f (PropAssignment.map g σ)

State before:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ (∃ σ_1, σ_1 ⊨ φ ∧ PropAssignment.map g σ = PropAssignment.map g σ_1) ∧
    PropAssignment.map (g ∘ f) σ = PropAssignment.map f (PropAssignment.map g σ)
Tactic:
simp [*, PropAssignment.map, Function.comp]
State after:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ (fun x => σ (g x)) = fun x => σ_1 (g x)

State before:
case h
ν' : Type u_3
inst✝¹ : Fintype ν'
ν'' : Type u_1
ν : Type u_2
inst✝ : Fintype ν''
f : ν'' → ν'
g : ν' → ν
φ : PropFun ν
σ : PropAssignment ν
h : σ ⊨ φ
⊢ ∃ σ_1, σ_1 ⊨ φ ∧ (fun x => σ (g x)) = fun x => σ_1 (g x)
Tactic:
use σ
State after:
no goals