Theorem: LO.FirstOrder.Structure.eval_ofEquiv_iff (Logic/FirstOrder/Basic/Semantics/Semantics.lean)

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
⊢ (Eval (ofEquiv φ) e ε) ⊤ ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) ⊤
Tactic:
simp
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
⊢ (Eval (ofEquiv φ) e ε) ⊥ ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) ⊥
Tactic:
simp
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (Semiformula.rel r v) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (Semiformula.rel r v)
Tactic:
simp [Function.comp, eval_rel, ofEquiv_rel φ, Structure.ofEquiv_val φ]
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (nrel r v) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (nrel r v)
Tactic:
simp [Function.comp, eval_nrel, ofEquiv_rel φ, Structure.ofEquiv_val φ]
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p q : Semiformula L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (p ⋏ q) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (p ⋏ q)
Tactic:
simp [eval_ofEquiv_iff (p := p), eval_ofEquiv_iff (p := q)]
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p q : Semiformula L μ x✝
⊢ (Eval (ofEquiv φ) e ε) (p ⋎ q) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (p ⋎ q)
Tactic:
simp [eval_ofEquiv_iff (p := p), eval_ofEquiv_iff (p := q)]
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (Eval (ofEquiv φ) e ε) (∀' p) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (∀' p)
Tactic:
simp
State after:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∀ (x : N), (Eval (ofEquiv φ) (x :> e) ε) p) ↔ ∀ (x : M), (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∀ (x : N), (Eval (ofEquiv φ) (x :> e) ε) p) ↔ ∀ (x : M), (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
exact
⟨fun h x => by simpa[Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp (h (φ x)),
fun h x => eval_ofEquiv_iff.mpr (by simpa[Matrix.comp_vecCons''] using h (φ.symm x))⟩
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
h : ∀ (x : N), (Eval (ofEquiv φ) (x :> e) ε) p
x : M
⊢ (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
simpa[Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp (h (φ x))
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
h : ∀ (x : M), (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
x : N
⊢ (Eval s (⇑φ.symm ∘ (x :> e)) (⇑φ.symm ∘ ε)) p
Tactic:
simpa[Matrix.comp_vecCons''] using h (φ.symm x)
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (Eval (ofEquiv φ) e ε) (∃' p) ↔ (Eval s (⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) (∃' p)
Tactic:
simp
State after:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∃ x, (Eval (ofEquiv φ) (x :> e) ε) p) ↔ ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∃ x, (Eval (ofEquiv φ) (x :> e) ε) p) ↔ ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
exact
⟨by rintro ⟨x, h⟩; exists φ.symm x; simpa[Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp h,
by rintro ⟨x, h⟩; exists φ x; apply eval_ofEquiv_iff.mpr; simpa[Matrix.comp_vecCons''] using h⟩
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∃ x, (Eval (ofEquiv φ) (x :> e) ε) p) → ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
rintro ⟨x, h⟩
State after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : N
h : (Eval (ofEquiv φ) (x :> e) ε) p
⊢ ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p

State before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : N
h : (Eval (ofEquiv φ) (x :> e) ε) p
⊢ ∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
exists φ.symm x
State after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : N
h : (Eval (ofEquiv φ) (x :> e) ε) p
⊢ (Eval s (φ.symm x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p

State before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : N
h : (Eval (ofEquiv φ) (x :> e) ε) p
⊢ (Eval s (φ.symm x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
Tactic:
simpa[Matrix.comp_vecCons''] using eval_ofEquiv_iff.mp h
State after:
no goals

State before:
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
⊢ (∃ x, (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p) → ∃ x, (Eval (ofEquiv φ) (x :> e) ε) p
Tactic:
rintro ⟨x, h⟩
State after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ ∃ x, (Eval (ofEquiv φ) (x :> e) ε) p

State before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ ∃ x, (Eval (ofEquiv φ) (x :> e) ε) p
Tactic:
exists φ x
State after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval (ofEquiv φ) (φ x :> e) ε) p

State before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval (ofEquiv φ) (φ x :> e) ε) p
Tactic:
apply eval_ofEquiv_iff.mpr
State after:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval s (⇑φ.symm ∘ (φ x :> e)) (⇑φ.symm ∘ ε)) p

State before:
case intro
M : Type u_2
N : Type u_1
L : Language
μ : Type v
μ₁ : Type v₁
μ₂ : Type v₂
s : Structure L M
φ : M ≃ N
x✝ : ℕ
e : Fin x✝ → N
ε : μ → N
p : Semiformula L μ (x✝ + 1)
x : M
h : (Eval s (x :> ⇑φ.symm ∘ e) (⇑φ.symm ∘ ε)) p
⊢ (Eval s (⇑φ.symm ∘ (φ x :> e)) (⇑φ.symm ∘ ε)) p
Tactic:
simpa[Matrix.comp_vecCons''] using h
State after:
no goals