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

State before:
L : Language
M : Type u_1
inst✝³ : Structure L M
inst✝² : L.Mul
inst✝¹ : Mul M
inst✝ : Structure.Mul L M
v : Fin 2 → M
⊢ func Language.Mul.mul v = v 0 * v 1
Tactic:
simpa[val_func, ←Matrix.fun_eq_vec₂] using
  Structure.Mul.mul (L := L) (v 0) (v 1)
State after:
no goals