simp
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
idx : Idx
c✝ : R
x✝ : Cont × Elem
⊢ (match c✝ • x✝ with
    | (cont, elem) => set cont idx elem) =
    c✝ •
      match x✝ with
      | (cont, elem) => set cont idx elem
case map_smul
K : Type
inst✝⁷ : RCLike K
Cont : Type
Idx Elem : outParam Type
inst✝⁶ : ArrayType Cont Idx Elem
inst✝⁵ : IndexType Idx
inst✝⁴ : LawfulIndexType Idx
inst✝³ : DecidableEq Idx
R : Type
inst✝² : CommSemiring R
inst✝¹ : AddCommGroup Elem
inst✝ : Module R Elem
idx : Idx
c✝ : R
x✝ : Cont × Elem
⊢ set (c✝ • x✝.1) idx (c✝ • x✝.2) = c✝ • set x✝.1 idx x✝.2