Theorem: LO.FirstOrder.Interpretation.sub_exists (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
⊢ ∃ x, ι.Dom x
Tactic:
simpa [Dom, models_iff, eval_substs, Matrix.constant_eq_singleton] using consequence_iff_add_eq.mp ι.domain_nonempty M inferInstance
State after:
no goals