x +ᵥ A = {x} + A

Stream: Is there code for X?

[Mitchell Lee]

Hello, is there any one-line proof of this in mathlib?

import Mathlib

open scoped Pointwise

example {M : Type} [Add M] (x : M) (A : Set M) : x +ᵥ A = {x} + A := by
  sorry

[Matt Diamond]

idk if there's a lemma, but you can solve it with by rw [Set.singleton_add]; rfl

[Mitchell Lee]

Thanks

[Yaël Dillies]

Yes that's supposed to be docs#Set.singleton_add but it's currently misstated. I have been trying to fix it for more than a year :smiling_face_with_tear: