no goals
I : Type u
α : Type ?u.12756
β : Type u_1
γ : Type ?u.12762
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x✝ y : (i : I) → f i
i✝ : I
inst✝⁴ : DecidableEq I
inst✝³ : (i : I) → One (f i)
inst✝² : (i : I) → One (g i)
inst✝¹ : (i : I) → One (h i)
inst✝ : One β
i : I
x : β
i' : I
⊢ mulSingle i x i' = mulSingle i' x i
simp [mulSingle_apply, eq_comm]