∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {l₁ l₂ : List α},
  (l₁ ++ l₂).partialProds = l₁.partialProds ++ List.map (fun x => l₁.prod * x) l₂.partialProds.tail