@[simp]

theorem indicator_one_smul {α : Type u_1} {G : Type u_2} {M₀ : Type u_3} [One M₀] [Zero M₀] [Group G] [MulAction G α] (g : G) (s : Set α) (a : α) : (g • s).indicator (fun (x : α) => 1) a = s.indicator (fun (x : α) => 1) (g⁻¹ • a)

@[simp]

theorem indicator_one_vadd {α : Type u_1} {G : Type u_2} {M₀ : Type u_3} [One M₀] [Zero M₀] [AddGroup G] [AddAction G α] (g : G) (s : Set α) (a : α) : (g +ᵥ s).indicator (fun (x : α) => 1) a = s.indicator (fun (x : α) => 1) (-g +ᵥ a)