∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] (x x_1 : ↥(NonUnitalSubsemiring.center α)),
  (let __src := AddMonoid.End.mulLeft ↑(x + x_1);
    ⟨{ toAddMonoidHom := AddMonoid.End.mulLeft ↑(x + x_1), map_mul_left' := ⋯, map_mul_right' := ⋯ }, ⋯⟩) =
    (let __src := AddMonoid.End.mulLeft ↑x;
      ⟨{ toAddMonoidHom := AddMonoid.End.mulLeft ↑x, map_mul_left' := ⋯, map_mul_right' := ⋯ }, ⋯⟩) +
      let __src := AddMonoid.End.mulLeft ↑x_1;
      ⟨{ toAddMonoidHom := AddMonoid.End.mulLeft ↑x_1, map_mul_left' := ⋯, map_mul_right' := ⋯ }, ⋯⟩