∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {x : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {ι' : Type u_6} {g : ι' → ι},
  Function.Surjective g → ProbabilityTheory.iIndep (m ∘ g) μ → ProbabilityTheory.iIndep m μ