Theorem: LO.FirstOrder.Semiformula.eval_hom_univClosure (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₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
⊢ (Evalf s₂ (⇑φ ∘ ε₁)) (∀* p) → (Evalf s₁ ε₁) (∀* p)
Tactic:
simp
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₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
⊢ (∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p) → ∀ (e : Fin n → M₁), (Eval s₁ e ε₁) p

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₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
⊢ (∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p) → ∀ (e : Fin n → M₁), (Eval s₁ e ε₁) p
Tactic:
intro h e₁
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₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
h : ∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p
e₁ : Fin n → M₁
⊢ (Eval s₁ e₁ ε₁) p

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₁
n : ℕ
ε₁ : μ → M₁
p : Semiformula L μ n
hp : p.Open
h : ∀ (e : Fin n → M₂), (Eval s₂ e (⇑φ ∘ ε₁)) p
e₁ : Fin n → M₁
⊢ (Eval s₁ e₁ ε₁) p
Tactic:
exact (eval_hom_iff_of_open φ hp).mpr (h (φ ∘ e₁))
State after:
no goals