Theorem: LO.FirstOrder.Semiformula.eval_hom_iff_of_open (Logic/FirstOrder/Basic/Semantics/Elementary.lean)

State before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
x✝ : ⊤.Open
⊢ (Eval s₁ e₁ ε₁) ⊤ ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) ⊤
Tactic:
simp
State after:
no goals

State before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
x✝ : ⊥.Open
⊢ (Eval s₁ e₁ ε₁) ⊥ ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) ⊥
Tactic:
simp
State after:
no goals

State before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝¹
x✝ : (rel r v).Open
⊢ (Eval s₁ e₁ ε₁) (rel r v) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (rel r v)
Tactic:
simp [Function.comp, eval_rel, ←EmbeddingClass.rel φ, HomClass.val_term]
State after:
no goals

State before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝¹ : ℕ
e₁ : Fin x✝¹ → M₁
ε₁ : μ → M₁
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L μ x✝¹
x✝ : (nrel r v).Open
⊢ (Eval s₁ e₁ ε₁) (nrel r v) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (nrel r v)
Tactic:
simp [Function.comp, eval_nrel, ←EmbeddingClass.rel φ, HomClass.val_term]
State after:
no goals

State before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : (p ⋏ q).Open
⊢ (Eval s₁ e₁ ε₁) (p ⋏ q) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (p ⋏ q)
Tactic:
simp at h ⊢
State after:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : p.Open ∧ q.Open
⊢ (Eval s₁ e₁ ε₁) p ∧ (Eval s₁ e₁ ε₁) q ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p ∧ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) q

State before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : p.Open ∧ q.Open
⊢ (Eval s₁ e₁ ε₁) p ∧ (Eval s₁ e₁ ε₁) q ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p ∧ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) q
Tactic:
simp [eval_hom_iff_of_open h.1, eval_hom_iff_of_open h.2]
State after:
no goals

State before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : (p ⋎ q).Open
⊢ (Eval s₁ e₁ ε₁) (p ⋎ q) ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) (p ⋎ q)
Tactic:
simp at h ⊢
State after:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : p.Open ∧ q.Open
⊢ (Eval s₁ e₁ ε₁) p ∨ (Eval s₁ e₁ ε₁) q ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p ∨ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) q

State before:
n : ℕ
μ : Type u_6
L : Language
M : Type u_1
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst✝⁵ : Nonempty M
inst✝⁴ : Nonempty M₁
inst✝³ : Nonempty M₂
inst✝² : Nonempty M₃
s : Structure L M
s₁ : Structure L M₁
s₂ : Structure L M₂
s₃ : Structure L M₃
F : Type u_5
inst✝¹ : FunLike F M₁ M₂
inst✝ : EmbeddingClass F L M₁ M₂
φ : F
e₁✝ : Fin n → M₁
ε₁✝ : μ → M₁
x✝ : ℕ
e₁ : Fin x✝ → M₁
ε₁ : μ → M₁
p q : Semiformula L μ x✝
h : p.Open ∧ q.Open
⊢ (Eval s₁ e₁ ε₁) p ∨ (Eval s₁ e₁ ε₁) q ↔ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) p ∨ (Eval s₂ (⇑φ ∘ e₁) (⇑φ ∘ ε₁)) q
Tactic:
simp [eval_hom_iff_of_open h.1, eval_hom_iff_of_open h.2]
State after:
no goals