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

State before:
Cont : Type u_3
Idx : outParam (Type u_4)
Elem : outParam (Type u_2)
inst✝⁴ : IndexType Idx
inst✝³ : outParam (DecidableEq Idx)
inst✝² : LawfulIndexType Idx
inst✝¹ : ArrayType Cont Idx Elem
R : Type u_1
inst✝ : SMul R Elem
r : R
x : Cont
i : Idx
⊢ (r • x)[i] = r • x[i]
Tactic:
simp[HSMul.hSMul,SMul.smul]
State after:
no goals