Theorem: LO.FirstOrder.uLift_elementaryEquiv (Logic/FirstOrder/Basic/Model.lean)

State before:
L : Language
M : Type v
inst✝¹ : Structure L M
inst✝ : Nonempty M
⊢ ULift.{v', v} M ≡ₑ[L] M
Tactic:
intro σ
State after:
L : Language
M : Type v
inst✝¹ : Structure L M
inst✝ : Nonempty M
σ : Sentence L
⊢ ULift.{v', v} M ⊧ₘ σ ↔ M ⊧ₘ σ

State before:
L : Language
M : Type v
inst✝¹ : Structure L M
inst✝ : Nonempty M
σ : Sentence L
⊢ ULift.{v', v} M ⊧ₘ σ ↔ M ⊧ₘ σ
Tactic:
simp [models_iff, Semiformula.evalm_uLift, Matrix.empty_eq, Empty.eq_elim]
State after:
no goals