theorem translate_indicator_one {G : Type u_1} (M₀ : Type u_2) [One M₀] [Zero M₀] [AddCommGroup G] (a : G) (s : Set G) : translate a (s.indicator fun (x : G) => 1) = (a +ᵥ s).indicator fun (x : G) => 1