ext
case map_add
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
x✝ y✝ : Cont × Elem
⊢ set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2) = set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2
case map_add.a
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
x✝ y✝ : Cont × Elem
i✝ : Idx
⊢ (set (x✝.1 + y✝.1) idx (x✝.2 + y✝.2))[i✝] = (set x✝.1 idx x✝.2 + set y✝.1 idx y✝.2)[i✝]