∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsMulLeftInvariant] [Countable ↥Γ] [ν.IsMulRightInvariant] [MeasureTheory.SigmaFinite ν] [μ.IsMulLeftInvariant]
  [MeasureTheory.SigmaFinite μ] {s : Set G},
  MeasureTheory.IsFundamentalDomain (↥Γ.op) s ν →
    ∀ {V : Set (G ⧸ Γ)},
      MeasurableSet V →
        μ V ≠ 0 → μ V = ν (QuotientGroup.mk ⁻¹' V ∩ s) → μ V ≠ ⊤ → MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ