Theorem: SciLean.ArrayType.mul_get (SciLean/Data/ArrayType/Basic.lean)

State before:
Cont : Type u_2
Idx : outParam (Type u_3)
Elem : outParam (Type u_1)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
inst✝ : Mul Elem
x y : Cont
i : Idx
⊢ (x * y)[i] = x[i] * y[i]
Tactic:
simp[HMul.hMul,Mul.mul]
State after:
no goals