Theorem: LO.FirstOrder.Interpretation.func_existsUnique_on_dom (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
k : ℕ
f : L'.Func k
⊢ ∀ (v : Fin k → M), (∀ (i : Fin k), ι.Dom (v i)) → ∃! y, ι.Dom y ∧ (Evalbm M (y :> v)) (ι.func f)
Tactic:
simpa [Dom, models_iff, eval_substs, Matrix.constant_eq_singleton] using consequence_iff_add_eq.mp (ι.func_defined f) M inferInstance
State after:
no goals