monoid structure on set G

Stream: maths

[Thomas Browning]

Does mathlib have this monoid struture on subsets of a monoid? If not, should I PR it?

variables {M : Type*} [monoid M]

instance : monoid (set M) :=
{ one := {1},
    mul := λ S T g, ∃ s ∈ S, ∃ t ∈ T, g = s * t,
    one_mul := begin
        intro S,
        ext g,
        split,
        { rintro ⟨t, ht, s, hs, hg⟩,
            rwa [hg, set.mem_singleton_iff.mp ht, one_mul] },
        { exact λ hg, ⟨1, set.mem_singleton 1, g, hg, (one_mul g).symm⟩ },
    end,
    mul_one := begin
        intro S,
        ext g,
        split,
        { rintro ⟨t, ht, s, hs, hg⟩,
            rwa [hg, set.mem_singleton_iff.mp hs, mul_one] },
        { exact λ hg, ⟨g, hg, 1, set.mem_singleton 1, (mul_one g).symm⟩ },
    end,
    mul_assoc := begin
        intros S T U,
        ext g,
        split,
        { rintros ⟨st, ⟨s, hs, t, ht, hst⟩, u, hu, hg⟩,
            exact ⟨s, hs, t * u, ⟨t, ht, u, hu, rfl⟩, by rw [hg, hst, mul_assoc]⟩ },
        { rintros ⟨s, hs, tu, ⟨t, ht, u, hu, htu⟩, hg⟩,
            exact ⟨s * t, ⟨s, hs, t, ht, rfl⟩, u, hu, by rw [hg, htu, mul_assoc]⟩ },
    end }

[Reid Barton]

Yes, it's in https://leanprover-community.github.io/mathlib_docs/algebra/pointwise.html