∀ (G : Type u_1) {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α),
  AddAction.aestabilizer G μ s = { carrier := {g | g +ᵥ s =ᵐ[μ] s}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }