simp[HSMul.hSMul, SMul.smul]
case a
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
K : Type u_1
inst✝ : SMul K Elem
f : Idx → Elem
a : K
⊢ ∀ (i : Idx), (a • Indexed.ofFn f)[i] = (Indexed.ofFn fun i => a • f i)[i]
no goals