∀ {G' : Type u_1} [inst : AddGroup G'] [inst_1 : MeasurableSpace G'] [inst_2 : TopologicalSpace G']
  [IsTopologicalAddGroup G'] [BorelSpace G'] {μ' : MeasureTheory.Measure G'} {Γ' : AddSubgroup G'} {𝓕' : Set G'},
  MeasureTheory.IsAddFundamentalDomain (↥Γ'.op) 𝓕' μ' →
    ∀ [Countable ↥Γ'] [inst_6 : MeasurableSpace (G' ⧸ Γ')] [BorelSpace (G' ⧸ Γ')] {K : Type u_2}
      [inst_8 : NormedField K] [inst_9 : NormedSpace ℝ K] [μ'.IsAddRightInvariant] {f : G' → K},
      MeasureTheory.Integrable f μ' →
        ∀ {g : G' ⧸ Γ' → K},
          MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) →
            essSup (fun x => ‖g x‖ₑ) (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) ≠ ⊤ →
              MeasureTheory.AEStronglyMeasurable (QuotientAddGroup.automorphize f)
                  (MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')) →
                ∫ (x : G'), g ↑x * f x ∂μ' =
                  ∫ (x : G' ⧸ Γ'),
                    g x *
                      QuotientAddGroup.automorphize f x ∂MeasureTheory.Measure.map QuotientAddGroup.mk (μ'.restrict 𝓕')