Theorem: LO.FirstOrder.Structure.exp_eq_of_lang (Logic/FirstOrder/Basic/Operator.lean)

State before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.Exp
inst✝¹ : Exp M
inst✝ : Structure.Exp L M
v : Fin 1 → M
⊢ func Language.Exp.exp v = exp (v 0)
Tactic:
simpa[val_func, ←Matrix.constant_eq_singleton'] using
  Structure.Exp.exp (L := L) (v 0)
State after:
no goals