no goals
L : Language
L' : Language
M : Type w
N : Type u_1
P : Type ?u.269466
inst✝² : Structure L M
inst✝¹ : Structure L N
inst✝ : Structure L P
α : Type u'
β : Type v'
n : ℕ
⊢ M ≅[L] N ↔ ∀ (φ : Sentence L), M ⊨ φ ↔ N ⊨ φ
simp only [ElementarilyEquivalent, Set.ext_iff, completeTheory, Set.mem_setOf_eq]