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

State before:
n✝ : ℕ
μ : Sort ?u.89010
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✝ : Structure.EmbeddingClass F L M₁ M₂
φ : F
e₁ : Fin n✝ → M₁
ε₁ : μ → M₁
n : ℕ
σ : Semisentence L n
hσ : Semiformula.Open σ
⊢ M₂ ⊧ₘ ∀* σ → M₁ ⊧ₘ ∀* σ
Tactic:
simpa[Matrix.empty_eq, Empty.eq_elim, models_iff] using
  Semiformula.eval_hom_univClosure (ε₁ := Empty.elim) φ hσ
State after:
no goals