∀ {G : Type u_3} {α : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (H : AddSubgroup G),
  MeasureTheory.VAddInvariantMeasure (↥H) α μ