Theorem: LO.FirstOrder.Structure.ElementaryEquiv.modelsTheory (Logic/FirstOrder/Basic/Semantics/Elementary.lean)

State before:
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₃
h : M₁ ≡ₑ[L] M₂
T : Theory L
⊢ M₁ ⊧ₘ* T ↔ M₂ ⊧ₘ* T
Tactic:
simp [modelsTheory_iff, h.models]
State after:
no goals