Theorem: LO.FirstOrder.Interpretation.models_translation_iff (Logic/FirstOrder/Interpretation.lean)

State before:
L L' : Language
inst✝³ : L.Eq
T : Theory L
ι : Interpretation T L'
M : Type u
inst✝² : Nonempty M
s : Structure L M
inst✝¹ : Structure.Eq L M
inst✝ : M ⊧ₘ* T
σ : Sentence L'
⊢ M ⊧ₘ ι.translation σ ↔ ι.Sub M ⊧ₘ σ
Tactic:
simp [models_iff, ←eval_translation_iff, Matrix.empty_eq]
State after:
no goals